---

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

.....aux..... 
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. Colinear(c;a;x)
24. a-x-c
⊢ ∃y':Point. (Colinear(a;c;y') ∧ ay' ≅ by)
BY
{ ((D 0 With ⌜x⌝  THEN Auto)
   THEN (((InstLemma `extend-using-SC` [⌜e⌝;⌜a⌝;⌜c⌝;⌜a⌝]⋅ THENA Auto) THEN ExRepD THEN RenameVar `I' (-3))
         THEN (InstLemma `extend-using-SC` [⌜e⌝;⌜b⌝;⌜c⌝;⌜b⌝]⋅ THENA Auto)
         THEN ExRepD
         THEN RenameVar `H' (-3))
   THEN ((InstLemma `extend-using-SC` [⌜e⌝;⌜a⌝;⌜b⌝;⌜a⌝]⋅ THENA Auto) THEN ExRepD THEN RenameVar `F' (-3))
   THEN (InstLemma `extend-using-SC` [⌜e⌝;⌜b⌝;⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN ExRepD
   THEN RenameVar `G' (-3)) }

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. Colinear(c;a;x)
24. a-x-c
25. Colinear(a;c;x)
26. I : Point
27. B(acI)
28. cI ≅ ca
29. H : Point
30. B(bcH)
31. cH ≅ cb
32. F : Point
33. B(abF)
34. bF ≅ ba
35. G : Point
36. B(baG)
37. aG ≅ ab
⊢ ax ≅ by

---

Latex:

---

Latex:
.....aux..... 
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.  Colinear(c;a;x)
24.  a-x-c
\mvdash{}  \mexists{}y':Point.  (Colinear(a;c;y')  \mwedge{}  ay'  \mcong{}  by)


By

---

Latex:
((D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)
  THEN  (((InstLemma  `extend-using-SC`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD
                THEN  RenameVar  `I'  (-3))
              THEN  (InstLemma  `extend-using-SC`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  ExRepD
              THEN  RenameVar  `H'  (-3))
  THEN  ((InstLemma  `extend-using-SC`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  ExRepD
              THEN  RenameVar  `F'  (-3))
  THEN  (InstLemma  `extend-using-SC`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  RenameVar  `G'  (-3))

---

Home Index