---

Step * 1 of Lemma common-P_point-intersecting-P_lines


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)
BY
{ (((InstHyp [⌜l⌝;⌜n⌝;⌜l1⌝] (11)⋅ THEN Auto) THEN D -1)
   THEN InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜l⌝;⌜l1⌝]⋅
   THEN Auto) }

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
16. l \/ l1
17. l \/ l1 ⇐ (l # l1) ∧ (∃x:Point. (x I l ∧ x I l1))
18. (l # l1)
19. ∃x:Point. (x I l ∧ x I l1)
⊢ ∃x:Point. ((x I l ∧ x I n) ∧ x I l1)

2
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
16. n \/ l1
17. l \/ l1 ⇒ ((l # l1) ∧ (∃x:Point. (x I l ∧ x I l1)))
18. l \/ l1 ⇐ (l # l1) ∧ (∃x:Point. (x I l ∧ x I l1))
⊢ ∃x:Point. ((x I l ∧ x I n) ∧ x I l1)

---

Latex:

---

Latex:

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  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l1@i
9.  \mneg{}P\_point-line-sep(e;<p,  l,  n,  P4,  P5><l1,  L1>)
10.  l  \mbackslash{}/  n
11.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
12.  (l  \#  n)
13.  x  :  Point
14.  x  I  l
15.  x  I  n
\mvdash{}  \mexists{}x:Point.  ((x  I  l  \mwedge{}  x  I  n)  \mwedge{}  x  I  l1)


By

---

Latex:
(((InstHyp  [\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{}]  (11)\mcdot{}  THEN  Auto)  THEN  D  -1)
  THEN  InstLemma  `geo-intersect-lines-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index