---

Step * of Lemma common-P_point-parallel-P_lines

∀e:EuclideanParPlane. ∀P:P_point(e). ∀L:P_line(e).
  ((¬P_point-line-sep(e;P;L))
  ⇒ (fst(snd(P)) || fst(snd(snd(P))) ∧ (∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))))
  ⇒ fst(L) || fst(snd(snd(P))))
BY
{ ((((Auto THEN D 2 THEN D 3 THEN D 4) THEN All Reduce) THEN D 0 THEN Auto)
   THEN ((D 8 THEN D 7) THEN Unfold `P_point-line-sep` 0)
   THEN AllReduce) }

1
1. e : EuclideanParPlane@i'
2. p : Point@i
3. l : Line@i
4. n : Line@i
5. P4 : p I n@i
6. P5 : p # l@i
7. l1 : Line@i
8. L1 : p:Point × n:{n:Line| p I n}  × p # l1@i
9. l || n
10. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
⊢ (l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1)

---

Latex:

---

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


By

---

Latex:
((((Auto  THEN  D  2  THEN  D  3  THEN  D  4)  THEN  All  Reduce)  THEN  D  0  THEN  Auto)
  THEN  ((D  8  THEN  D  7)  THEN  Unfold  `P\_point-line-sep`  0)
  THEN  AllReduce)

---

Home Index