---

Step * 1 1 1 1 2 1 1 3 of Lemma AX3


1. e : EuclideanParPlane@i'
2. l2 : Line@i
3. p1 : Point@i
4. l4 : n:{n:Line| p1 I n}  × p1 # l2@i
5. l1 : Line@i
6. p : Point@i
7. m2 : n:{n:Line| p I n}  × p # l1@i
8. p2 : Point@i
9. l : Line@i
10. n : Line@i
11. P4 : p2 I n@i
12. P5 : p2 # l@i
13. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
14. l \/ l1
15. ∀x:{x:Point| x I l ∧ x I n} . x # l1
16. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
17. l \/ l2
18. l2 \/ n
19. l2 \/ l
20. l2 \/ l1
21. l1 \/ l2 ⇐ (l1 # l2) ∧ (∃x:Point. (x I l1 ∧ x I l2))
22. p3 : Point
23. Colinear(p3;fst(l1);fst(snd(l1)))
24. p3 # fst(l2)fst(snd(l2))
25. x : Point
26. x I l1
27. x I l2
28. S1 : p3 I l1
29. S2 : p3 # l2
30. ¬P_point-line-sep(e;<p3, l2, l1, S1, S2>;<l2, p1, l4>)
31. l2 \/ l1
32. ∀x:{x:Point| x I l2 ∧ x I l1} . x # l1
⊢ False
BY
{ ((((InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜l2⌝;⌜l1⌝]⋅ THEN Auto) THEN ExRepD) THEN InstHyp [⌜x1⌝] (32)⋅ THEN Auto)
   THEN InstLemma `geo-incident-not-plsep` [⌜e⌝;⌜x1⌝;⌜l1⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane@i'
2.  l2  :  Line@i
3.  p1  :  Point@i
4.  l4  :  n:\{n:Line|  p1  I  n\}    \mtimes{}  p1  \#  l2@i
5.  l1  :  Line@i
6.  p  :  Point@i
7.  m2  :  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l1@i
8.  p2  :  Point@i
9.  l  :  Line@i
10.  n  :  Line@i
11.  P4  :  p2  I  n@i
12.  P5  :  p2  \#  l@i
13.  \mneg{}((l  \mbackslash{}/  l2  \mvee{}  n  \mbackslash{}/  l2)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l2))
14.  l  \mbackslash{}/  l1
15.  \mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l1
16.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
17.  l  \mbackslash{}/  l2
18.  l2  \mbackslash{}/  n
19.  l2  \mbackslash{}/  l
20.  l2  \mbackslash{}/  l1
21.  l1  \mbackslash{}/  l2  \mLeftarrow{}{}  (l1  \#  l2)  \mwedge{}  (\mexists{}x:Point.  (x  I  l1  \mwedge{}  x  I  l2))
22.  p3  :  Point
23.  Colinear(p3;fst(l1);fst(snd(l1)))
24.  p3  \#  fst(l2)fst(snd(l2))
25.  x  :  Point
26.  x  I  l1
27.  x  I  l2
28.  S1  :  p3  I  l1
29.  S2  :  p3  \#  l2
30.  \mneg{}P\_point-line-sep(e;<p3,  l2,  l1,  S1,  S2><l2,  p1,  l4>)
31.  l2  \mbackslash{}/  l1
32.  \mforall{}x:\{x:Point|  x  I  l2  \mwedge{}  x  I  l1\}  .  x  \#  l1
\mvdash{}  False


By

---

Latex:
((((InstLemma  `geo-intersect-lines-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l2\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{}]\mcdot{}  THEN  Auto)  THEN  ExRepD)
    THEN  InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (32)\mcdot{}
    THEN  Auto)
  THEN  InstLemma  `geo-incident-not-plsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index