---

Step * of Lemma geo-sum-eq-x

No Annotations
∀e:BasicGeometry. ∀a,b,c,d:Point.  ((X = |ab| + |cd| ∈ Length) ⇒ (a ≡ b ∧ c ≡ d))
BY
{ (InstLemma `geo-length-null-segment` [] THEN RepeatFor 2 (ParallelLast'⋅) THEN RepeatFor 5 ((D 0 THENA Auto))) }

1
1. e : BasicGeometry
2. a : Point
3. |aa| = X ∈ Length
4. b : Point
5. c : Point
6. d : Point
7. X = |ab| + |cd| ∈ Length
⊢ a ≡ b

2
1. e : BasicGeometry
2. a : Point
3. |aa| = X ∈ Length
4. b : Point
5. c : Point
6. d : Point
7. X = |ab| + |cd| ∈ Length
⊢ c ≡ d

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:BasicGeometry.  \mforall{}a,b,c,d:Point.    ((X  =  |ab|  +  |cd|)  {}\mRightarrow{}  (a  \mequiv{}  b  \mwedge{}  c  \mequiv{}  d))


By

---

Latex:
(InstLemma  `geo-length-null-segment`  []
  THEN  RepeatFor  2  (ParallelLast'\mcdot{})
  THEN  RepeatFor  5  ((D  0  THENA  Auto)))

---

Home Index