---

Step * 1 1 1 of Lemma proj-point-sep_defB


1. e : EuclideanParPlane
2. x1 : Point
3. x2 : Point
4. x3 : Point
5. y : Point
6. x5 : x3 ≠ y
7. ¬x1 # x3y
8. x2 # x3y
9. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
10. x2 # x3y ⇐ (∀x:Point. (Colinear(x;x3;y) ⇒ x2 ≠ x)) ∧ x3 ≠ y
11. ∀x:Point. (Colinear(x;x3;y) ⇒ x2 ≠ x)
12. x3 ≠ y
⊢ x1 ≠ x2
BY
{ (FLemma `not-lsep-iff-colinear` [7] THEN Auto) }

1
1. e : EuclideanParPlane
2. x1 : Point
3. x2 : Point
4. x3 : Point
5. y : Point
6. x5 : x3 ≠ y
7. ¬x1 # x3y
8. x2 # x3y
9. ∀l,m:Line.  (l \/ m ⇒ (∀n:Line. (l \/ n ∨ m \/ n)))
10. x2 # x3y ⇐ (∀x:Point. (Colinear(x;x3;y) ⇒ x2 ≠ x)) ∧ x3 ≠ y
11. ∀x:Point. (Colinear(x;x3;y) ⇒ x2 ≠ x)
12. x3 ≠ y
13. Colinear(x1;x3;y)
⊢ x1 ≠ x2

---

Latex:

---

Latex:

1.  e  :  EuclideanParPlane
2.  x1  :  Point
3.  x2  :  Point
4.  x3  :  Point
5.  y  :  Point
6.  x5  :  x3  \mneq{}  y
7.  \mneg{}x1  \#  x3y
8.  x2  \#  x3y
9.  \mforall{}l,m:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (\mforall{}n:Line.  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))
10.  x2  \#  x3y  \mLeftarrow{}{}  (\mforall{}x:Point.  (Colinear(x;x3;y)  {}\mRightarrow{}  x2  \mneq{}  x))  \mwedge{}  x3  \mneq{}  y
11.  \mforall{}x:Point.  (Colinear(x;x3;y)  {}\mRightarrow{}  x2  \mneq{}  x)
12.  x3  \mneq{}  y
\mvdash{}  x1  \mneq{}  x2


By

---

Latex:
(FLemma  `not-lsep-iff-colinear`  [7]  THEN  Auto)

---

Home Index