---

Step * 1 3 of Lemma common-P_point-parallel-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. l || n
10. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
11. l1 \/ n
12. l1 \/ l ∨ n \/ l
13. l \/ l1 ∨ n \/ l1
14. x : Point@i
15. [%7] : x I l ∧ x I n@i
⊢ x # l1
BY
{ ((Assert ⌜False⌝⋅ THEN Auto)
   THEN (InstLemma `geo-intersect-lines-iff` [⌜e⌝;⌜n⌝;⌜l⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (D -1)
   THEN EAuto 2) }

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
12. l1 \/ l ∨ n \/ l
13. l \/ l1 ∨ n \/ l1
14. x : Point@i
15. x I l
16. x I n
17. n \/ l ⇒ ((n # l) ∧ (∃x:Point. (x I n ∧ x I l)))
⊢ (n # l)

---

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.  l  ||  n
10.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
11.  l1  \mbackslash{}/  n
12.  l1  \mbackslash{}/  l  \mvee{}  n  \mbackslash{}/  l
13.  l  \mbackslash{}/  l1  \mvee{}  n  \mbackslash{}/  l1
14.  x  :  Point@i
15.  [\%7]  :  x  I  l  \mwedge{}  x  I  n@i
\mvdash{}  x  \#  l1


By

---

Latex:
((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `geo-intersect-lines-iff`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (D  -1)
  THEN  EAuto  2)

---

Home Index