---

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


1. e : EuclideanParPlane
2. x2 : Point
3. p : Point
4. l : Line
5. n : Line
6. P4 : p I n
7. P5 : p # l
8. l2 : Line
9. L3 : p:Point × n:{n:Line| p I n}  × p # l2
10. l1 : Line
11. L2 : p:Point × n:{n:Line| p I n}  × p # l1
12. ¬((l \/ l2 ∨ n \/ l2) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l2))
13. ¬((l \/ l1 ∨ n \/ l1) ∧ (∀x:{x:Point| x I l ∧ x I n} . x # l1))
14. l2 \/ l1
15. ∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n))
16. l1 \/ l
17. l1 \/ n
18. (l1 # l)
19. x : Point
20. x I l1
21. x I l
22. x I l
23. x # n
24. (l1 # n)
25. x1 : Point
26. x2 I l1
27. x2 I n
28. l \/ n
29. (l # n)
30. x2 I l
31. x2 I n
32. x1 ≡ x2
⊢ False
BY
{ ((InstLemma `geo-intersect-unique` [⌜e⌝;⌜l1⌝;⌜l⌝;⌜x⌝;⌜x2⌝]⋅ THEN Auto)
   THEN (RWO "-1" (23) THEN Auto)
   THEN InstLemma `geo-incident-not-plsep` [⌜e⌝;⌜x2⌝;⌜n⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x2  :  Point
3.  p  :  Point
4.  l  :  Line
5.  n  :  Line
6.  P4  :  p  I  n
7.  P5  :  p  \#  l
8.  l2  :  Line
9.  L3  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l2
10.  l1  :  Line
11.  L2  :  p:Point  \mtimes{}  n:\{n:Line|  p  I  n\}    \mtimes{}  p  \#  l1
12.  \mneg{}((l  \mbackslash{}/  l2  \mvee{}  n  \mbackslash{}/  l2)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l2))
13.  \mneg{}((l  \mbackslash{}/  l1  \mvee{}  n  \mbackslash{}/  l1)  \mwedge{}  (\mforall{}x:\{x:Point|  x  I  l  \mwedge{}  x  I  n\}  .  x  \#  l1))
14.  l2  \mbackslash{}/  l1
15.  \mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n))
16.  l1  \mbackslash{}/  l
17.  l1  \mbackslash{}/  n
18.  (l1  \#  l)
19.  x  :  Point
20.  x  I  l1
21.  x  I  l
22.  x  I  l
23.  x  \#  n
24.  (l1  \#  n)
25.  x1  :  Point
26.  x2  I  l1
27.  x2  I  n
28.  l  \mbackslash{}/  n
29.  (l  \#  n)
30.  x2  I  l
31.  x2  I  n
32.  x1  \mequiv{}  x2
\mvdash{}  False


By

---

Latex:
((InstLemma  `geo-intersect-unique`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}l1\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (RWO  "-1"  (23)  THEN  Auto)
  THEN  InstLemma  `geo-incident-not-plsep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index