---

Step * 1 of Lemma geo-incident-not-plsep


1. e : EuclideanPlane
2. x : Point
3. m : Line
4. x I m
⊢ ¬x # m
BY
{ ((RWO "geo-incident-line" (-1) THENA Auto) THEN GetLinePoints (-2) THEN RepUR ``geo-plsep`` 0 THEN Reduce (-1)⋅) }

1
1. e : EuclideanPlane
2. x : Point
3. x1 : Point
4. y : Point
5. m2 : x1 ≠ y
6. Colinear(x;x1;y)
⊢ ¬x # x1y

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  x  :  Point
3.  m  :  Line
4.  x  I  m
\mvdash{}  \mneg{}x  \#  m


By

---

Latex:
((RWO  "geo-incident-line"  (-1)  THENA  Auto)
  THEN  GetLinePoints  (-2)
  THEN  RepUR  ``geo-plsep``  0
  THEN  Reduce  (-1)\mcdot{})

---

Home Index