---

Step * of Lemma geo-add-length-implies-eq2

∀[e:BasicGeometry]. ∀[x:Length]. ∀[a,b:Point].  a ≡ b supposing x = x + |ab| + |ab| ∈ Length
BY
{ (Auto THEN (FLemma `geo-add-length-implies-eq-zero` [-1] THENA Auto)) }

1
1. e : BasicGeometry
2. x : Length
3. a : Point
4. b : Point
5. x = x + |ab| + |ab| ∈ Length
6. |ab| + |ab| = 0 ∈ Length
⊢ a ≡ b

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[x:Length].  \mforall{}[a,b:Point].    a  \mequiv{}  b  supposing  x  =  x  +  |ab|  +  |ab|


By

---

Latex:
(Auto  THEN  (FLemma  `geo-add-length-implies-eq-zero`  [-1]  THENA  Auto))

---

Home Index