---

Step * 1 2 1 of Lemma proj-point-sep_defA


1. e : EuclideanParPlane
2. x : Point
3. x1 : Point
4. x ≠ x1
5. m : Line
6. x I m
7. x1 # m
8. x # m
⊢ False
BY
{ (MoveToConcl (-1) THEN Fold `not` 0 THEN EAuto 1) }

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x  :  Point
3.  x1  :  Point
4.  x  \mneq{}  x1
5.  m  :  Line
6.  x  I  m
7.  x1  \#  m
8.  x  \#  m
\mvdash{}  False


By

---

Latex:
(MoveToConcl  (-1)  THEN  Fold  `not`  0  THEN  EAuto  1)

---

Home Index