---

Step * 1 1 2 1 1 1 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. n \/ 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. n \/ l2
18. n \/ l
19. ∃x:Point. ((x I fst(snd(<p2, l, n, P4, P5>)) ∧ x I fst(snd(snd(<p2, l, n, P4, P5>)))) ∧ x I fst(<l2, p1, l4>))
⊢ ∃P:P_point(e). ((¬P_point-line-sep(e;P;<l2, p1, l4>)) ∧ (¬P_point-line-sep(e;P;<l1, p, m2>)))
BY
{ (((ExRepD THEN Assert ⌜x I l2⌝⋅ THEN Auto) THEN Assert ⌜x # l1⌝⋅ THEN Auto)
   THEN (RenameVar `S1' (23) THEN RenameVar `S2' (24))
   THEN (D 0 With ⌜<x, l1, l2, S1, S2>⌝  THENA Auto)) }

1
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. n \/ 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. n \/ l2
18. n \/ l
19. x : Point
20. x I fst(snd(<p2, l, n, P4, P5>))
21. x I fst(snd(snd(<p2, l, n, P4, P5>)))
22. x I fst(<l2, p1, l4>)
23. S1 : x I l2
24. S2 : x # l1
⊢ (¬P_point-line-sep(e;<x, l1, l2, S1, S2>;<l2, p1, l4>)) ∧ (¬P_point-line-sep(e;<x, l1, l2, S1, S2>;<l1, p, m2>))

---

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.  n  \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.  n  \mbackslash{}/  l2
18.  n  \mbackslash{}/  l
19.  \mexists{}x:Point.  ((x  I  fst(snd(<p2,  l,  n,  P4,  P5>))  \mwedge{}  x  I  fst(snd(snd(<p2,  l,  n,  P4,  P5>))))  \mwedge{}  x  I  fst(\000C<l2,  p1,  l4>))
\mvdash{}  \mexists{}P:P\_point(e).  ((\mneg{}P\_point-line-sep(e;P;<l2,  p1,  l4>))  \mwedge{}  (\mneg{}P\_point-line-sep(e;P;<l1,  p,  m2>)))


By

---

Latex:
(((ExRepD  THEN  Assert  \mkleeneopen{}x  I  l2\mkleeneclose{}\mcdot{}  THEN  Auto)  THEN  Assert  \mkleeneopen{}x  \#  l1\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (RenameVar  `S1'  (23)  THEN  RenameVar  `S2'  (24))
  THEN  (D  0  With  \mkleeneopen{}<x,  l1,  l2,  S1,  S2>\mkleeneclose{}    THENA  Auto))

---

Home Index