---

Step * of Lemma common-P_point-intersecting-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))))
  ⇒ (∃x:Point. ((x I fst(snd(P)) ∧ x I fst(snd(snd(P)))) ∧ x I fst(L))))
BY
{ ((Auto THEN D 2 THEN (D 3 THEN D 4) THEN D 6)
   THEN All Reduce
   THEN (InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜l⌝;⌜n⌝]⋅ THEN Auto)
   THEN Thin (-3)
   THEN ExRepD) }

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. ¬P_point-line-sep(e;<p, l, n, P4, P5>;<l1, L1>)
10. l \/ n
11. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
12. (l # n)
13. x : Point
14. x I l
15. x I n
⊢ ∃x:Point. ((x I l ∧ x I n) ∧ x I 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))  \mbackslash{}/  fst(snd(snd(P)))  \mwedge{}  (\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))))


By

---

Latex:
((Auto  THEN  D  2  THEN  (D  3  THEN  D  4)  THEN  D  6)
  THEN  All  Reduce
  THEN  (InstLemma  `geo-intersect-lines-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  Thin  (-3)
  THEN  ExRepD)

---

Home Index