---

Step * 1 1 2 of Lemma Euclid-Prop2-lemma


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a # b
5. v : Point
6. c : Point
7. cb ≅ ab
8. ca ≅ ba
9. ca ≅ cb
10. c leftof ab
11. y : Point
12. B(cby)
13. by ≅ bv
14. v1 : Point
15. cv1 ≅ cy
16. B(acv1)
17. c # y ⇒ c # v1
18. x : Point
19. cx ≅ cy
20. B(xcv1)
21. Colinear(a;c;x)
22. c # y ⇒ x # v1
23. xa ≅ yb
⊢ ax ≅ bv
BY
{ ((FLemma `geo-congruent-symmetry` [-1] THENA Auto)
   THEN (Assert xa ≅ ax BY
               Auto)
   THEN FLemma `geo-congruent-transitivity` [-1;-2]
   THEN Auto
   THEN (FLemma `geo-congruent-symmetry` [13] THENA Auto)
   THEN (Assert by ≅ yb BY
               Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. a # b
5. v : Point
6. c : Point
7. cb ≅ ab
8. ca ≅ ba
9. ca ≅ cb
10. c leftof ab
11. y : Point
12. B(cby)
13. by ≅ bv
14. v1 : Point
15. cv1 ≅ cy
16. B(acv1)
17. c # y ⇒ c # v1
18. x : Point
19. cx ≅ cy
20. B(xcv1)
21. Colinear(a;c;x)
22. c # y ⇒ x # v1
23. xa ≅ yb
24. yb ≅ xa
25. xa ≅ ax
26. yb ≅ ax
27. bv ≅ by
28. by ≅ yb
⊢ ax ≅ bv

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  a  \#  b
5.  v  :  Point
6.  c  :  Point
7.  cb  \mcong{}  ab
8.  ca  \mcong{}  ba
9.  ca  \mcong{}  cb
10.  c  leftof  ab
11.  y  :  Point
12.  B(cby)
13.  by  \mcong{}  bv
14.  v1  :  Point
15.  cv1  \mcong{}  cy
16.  B(acv1)
17.  c  \#  y  {}\mRightarrow{}  c  \#  v1
18.  x  :  Point
19.  cx  \mcong{}  cy
20.  B(xcv1)
21.  Colinear(a;c;x)
22.  c  \#  y  {}\mRightarrow{}  x  \#  v1
23.  xa  \mcong{}  yb
\mvdash{}  ax  \mcong{}  bv


By

---

Latex:
((FLemma  `geo-congruent-symmetry`  [-1]  THENA  Auto)
  THEN  (Assert  xa  \mcong{}  ax  BY
                          Auto)
  THEN  FLemma  `geo-congruent-transitivity`  [-1;-2]
  THEN  Auto
  THEN  (FLemma  `geo-congruent-symmetry`  [13]  THENA  Auto)
  THEN  (Assert  by  \mcong{}  yb  BY
                          Auto))

---

Home Index