---

Step * 3 of Lemma geo-intersect-lines-iff


1. e : EuclideanPlane
2. p : Line
3. l : Line
4. geo-line-sep(e;p;l)
5. ∃x:Point. (x I p ∧ x I l)
⊢ p \/ l
BY
{ (GetLinePoints 3
   THEN GetLinePoints 2
   THEN (RWO "geo-incident-line" (-1) THENA Auto)
   THEN Reduce -1
   THEN D -1
   THEN RenameVar `a' (-2)
   THEN D -3
   THEN All
   Reduce⋅) }

1
1. e : EuclideanPlane
2. x1 : Point
3. y1 : Point
4. p2 : x1 ≠ y1
5. x : Point
6. y : Point
7. l2 : x ≠ y
8. p : Point
9. Colinear(p;x1;y1) ∧ p # xy
10. a : Point
11. Colinear(a;x1;y1) ∧ Colinear(a;x;y)
⊢ <x1, y1, p2> \/ <x, y, l2>

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  p  :  Line
3.  l  :  Line
4.  geo-line-sep(e;p;l)
5.  \mexists{}x:Point.  (x  I  p  \mwedge{}  x  I  l)
\mvdash{}  p  \mbackslash{}/  l


By

---

Latex:
(GetLinePoints  3
  THEN  GetLinePoints  2
  THEN  (RWO  "geo-incident-line"  (-1)  THENA  Auto)
  THEN  Reduce  -1
  THEN  D  -1
  THEN  RenameVar  `a'  (-2)
  THEN  D  -3
  THEN  All
  Reduce\mcdot{})

---

Home Index