---

Step * 1 of Lemma Euclid-Prop27


1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. Colinear(x;a;b)
9. Colinear(y;c;d)
10. a # b
11. c # d
12. a leftof yx
13. c leftof xy
14. axy ≅a cyx
15. ∃x,y:{z:Point| Colinear(z;a;b)} . (x leftof cd ∧ y leftof dc)
⊢ False
BY
{ (ExRepD
   THEN ((InstLemma  `use-plane-sep_strict` [⌜e⌝;⌜c⌝;⌜d⌝;⌜x1⌝;⌜y1⌝]⋅ THEN Auto) THEN ExRepD)
   THEN (Assert Colinear(x2;x;a) BY
               ((((D 16 THEN D 15) THEN Unhide) THEN Auto)
                THEN (Assert Colinear(a;x;y1) BY
                            Auto)
                THEN (Assert Colinear(a;x;x1) BY
                            Auto)))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. x : Point
7. y : Point
8. Colinear(x;a;b)
9. Colinear(y;c;d)
10. a # b
11. c # d
12. a leftof yx
13. c leftof xy
14. axy ≅a cyx
15. x1 : {z:Point| Colinear(z;a;b)} 
16. y1 : {z:Point| Colinear(z;a;b)} 
17. x1 leftof cd
18. y1 leftof dc
19. x2 : Point
20. Colinear(c;d;x2)
21. x1-x2-y1
22. Colinear(x2;x;a)
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  x  :  Point
7.  y  :  Point
8.  Colinear(x;a;b)
9.  Colinear(y;c;d)
10.  a  \#  b
11.  c  \#  d
12.  a  leftof  yx
13.  c  leftof  xy
14.  axy  \mcong{}\msuba{}  cyx
15.  \mexists{}x,y:\{z:Point|  Colinear(z;a;b)\}  .  (x  leftof  cd  \mwedge{}  y  leftof  dc)
\mvdash{}  False


By

---

Latex:
(ExRepD
  THEN  ((InstLemma    `use-plane-sep\_strict`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}y1\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
  THEN  (Assert  Colinear(x2;x;a)  BY
                          ((((D  16  THEN  D  15)  THEN  Unhide)  THEN  Auto)
                            THEN  (Assert  Colinear(a;x;y1)  BY
                                                    Auto)
                            THEN  (Assert  Colinear(a;x;x1)  BY
                                                    Auto))))

---

Home Index