---

Step * 1 2 2 of Lemma common-P_point-intersecting-P_lines2


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))
14. l1 \/ l
15. l \/ n
⊢ ∃x:Point. ((x I l ∧ x I n) ∧ x I l2 ∧ x I l1)
BY
{ ((InstLemma `common-P_point-intersecting-P_lines` [⌜e⌝;⌜<p, l, n, P3>⌝;⌜<l2, L3>⌝]⋅ THEN Auto)
   THEN (InstLemma `common-P_point-intersecting-P_lines` [⌜e⌝;⌜<p, l, n, P4, P5>⌝;⌜<l1, L2>⌝]⋅ THEN Auto)
   THEN (All Reduce THEN ExRepD)
   THEN (D 0 With ⌜x⌝  THEN Auto)
   THEN (InstLemma `geo-intersect-unique` [⌜e⌝;⌜l⌝;⌜n⌝;⌜x1⌝;⌜x⌝]⋅ THEN Auto)
   THEN RWO "-1" (20)
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  p  :  Point
3.  l  :  Line
4.  n  :  Line
5.  P3  :  p  I  n  \mwedge{}  p  \#  l
6.  l2  :  Line
7.  L3  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l2
8.  l1  :  Line
9.  L2  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l1
10.  \mneg{}((l  \mbackslash{}/  l2  \mvee{}  n  \mbackslash{}/  l2)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l2))
11.  \mneg{}((l  \mbackslash{}/  l1  \mvee{}  n  \mbackslash{}/  l1)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l1))
12.  l2  \mbackslash{}/  l1
13.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
14.  l1  \mbackslash{}/  l
15.  l  \mbackslash{}/  n
\mvdash{}  \mexists{}x:Point.  ((x  I  l  \mwedge{}  x  I  n)  \mwedge{}  x  I  l2  \mwedge{}  x  I  l1)


By

---

Latex:
((InstLemma  `common-P\_point-intersecting-P\_lines`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}<p,  l,  n,  P3>\mkleeneclose{};\mkleeneopen{}<l2,  L3>\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `common-P\_point-intersecting-P\_lines`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}<p,  l,  n,  P4,  P5>\mkleeneclose{};\mkleeneopen{}<l1,  L2>\mkleeneclose{}]\mcdot{}
              THEN  Auto
              )
  THEN  (All  Reduce  THEN  ExRepD)
  THEN  (D  0  With  \mkleeneopen{}x\mkleeneclose{}    THEN  Auto)
  THEN  (InstLemma  `geo-intersect-unique`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  RWO  "-1"  (20)
  THEN  Auto)

---

Home Index