---

Step * of Lemma common-P_point-intersecting-P_lines2

∀e:EuclideanParPlane. ∀P:P_point(e). ∀L,L1:P_line(e).
  (((¬P_point-line-sep(e;P;L)) ∧ (¬P_point-line-sep(e;P;L1)))
  ⇒ fst(L) \/ fst(L1)
  ⇒ (∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n)))
  ⇒ (∃x:Point. ((x I fst(snd(P)) ∧ x I fst(snd(snd(P)))) ∧ x I fst(L) ∧ x I fst(L1))))
BY
{ ((Auto THEN (D 2 THEN D 3 THEN D 4) THEN D 7 THEN D 6)
   THEN All Reduce
   THEN (Unfold `P_point-line-sep` 10 THEN Reduce 11)
   THEN Unfold `P_point-line-sep` 11
   THEN All Reduce) }

1
1. e : EuclideanParPlane
2. p : Point
3. l : Line
4. n : Line
5. P3 : p I n ∧ p # l
6. l2 : Line
7. L3 : p:Point × n:{n:Line| p I n}  × p # l2
8. l1 : Line
9. L2 : p:Point × n:{n:Line| p I n}  × p # l1
10. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
11. ¬((l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1))
12. l2 \/ l1
13. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
⊢ ∃x:Point. ((x I l ∧ x I n) ∧ x I l2 ∧ x I l1)

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  (D  2  THEN  D  3  THEN  D  4)  THEN  D  7  THEN  D  6)
  THEN  All  Reduce
  THEN  (Unfold  `P\_point-line-sep`  10  THEN  Reduce  11)
  THEN  Unfold  `P\_point-line-sep`  11
  THEN  All  Reduce)

---

Home Index