---

Step * of Lemma eu-three-segment

∀e:EuclideanPlane. ∀[a,b,c,A,B,C:Point].  (ac=AC) supposing (bc=BC and ab=AB and A_B_C and a_b_c and (¬(a = b ∈ Point)))
BY
{ (InstLemma `eu-five-segment` []
   THEN RepeatFor 4 (ParallelLast')
   THEN (With ⌜a⌝ (D (-1))⋅ THENA Auto)
   THEN RepeatFor 3 (ParallelLast')
   THEN (With ⌜A⌝ (D (-1))⋅ THENA Auto)
   THEN RepeatFor 5 ((ParallelLast' THENA Auto))) }

1
1. e : EuclideanPlane@i'
2. [a] : Point
3. [b] : Point
4. [c] : Point
5. [A] : Point
6. [B] : Point
7. [C] : Point
8. ¬(a = b ∈ Point)
9. [%] : a_b_c
10. [%4] : A_B_C
11. [%6] : ab=AB
12. [%8] : bc=BC
13. (ca=CA) supposing (ba=BA and aa=AA)
⊢ ac=AC

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,A,B,C:Point].    (ac=AC)  supposing  (bc=BC  and  ab=AB  and  A\_B\_C  and  a\_b\_c  and  (\mneg{}(a  =  b)))


By

---

Latex:
(InstLemma  `eu-five-segment`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  (With  \mkleeneopen{}a\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (With  \mkleeneopen{}A\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  RepeatFor  5  ((ParallelLast'  THENA  Auto)))

---

Home Index