---

Step * of Lemma AX3

∀e:EuclideanParPlane. ∀l,m:P_line(e).
  ((P_line-sep(e;l;m) ∧ (∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))))
  ⇒ (∃P:P_point(e). ((¬P_point-line-sep(e;P;l)) ∧ (¬P_point-line-sep(e;P;m)))))
BY
{ (Auto
   THEN ((Unfold `P_line-sep` -2 THEN ExRepD) THEN D 3 THEN D 4)
   THEN ((D 2 THEN D 3) THEN (D 8 THEN D 9) THEN D 10)
   THEN All Reduce) }

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. P3 : p2 I n ∧ p2 # l@i
12. ¬P_point-line-sep(e;<p2, l, n, P3>;<l2, p1, l4>)
13. P_point-line-sep(e;<p2, l, n, P3>;<l1, p, m2>)
14. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
⊢ ∃P:P_point(e). ((¬P_point-line-sep(e;P;<l2, p1, l4>)) ∧ (¬P_point-line-sep(e;P;<l1, p, m2>)))

---

Latex:

---

Latex:
\mforall{}e:EuclideanParPlane.  \mforall{}l,m:P\_line(e).
    ((P\_line-sep(e;l;m)  \mwedge{}  (\mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))))
    {}\mRightarrow{}  (\mexists{}P:P\_point(e).  ((\mneg{}P\_point-line-sep(e;P;l))  \mwedge{}  (\mneg{}P\_point-line-sep(e;P;m)))))


By

---

Latex:
(Auto
  THEN  ((Unfold  `P\_line-sep`  -2  THEN  ExRepD)  THEN  D  3  THEN  D  4)
  THEN  ((D  2  THEN  D  3)  THEN  (D  8  THEN  D  9)  THEN  D  10)
  THEN  All  Reduce)

---

Home Index