∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [Nonempty Z] [inst : MetricSpace Z] [inst_1 : MetricSpace X]
  [inst_2 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y},
  Isometry Φ →
    Isometry Ψ → ∀ (x y z : X ⊕ Y), Metric.glueDist Φ Ψ 0 x z ≤ Metric.glueDist Φ Ψ 0 x y + Metric.glueDist Φ Ψ 0 y z