---

Step * 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)))
⊢ x1 ≠ x2
BY
{ (InstLemma `lsep-iff-all-sep` [⌜e⌝;⌜x2⌝;⌜x3⌝;⌜y⌝]⋅ 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
⊢ 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)))
\mvdash{}  x1  \mneq{}  x2


By

---

Latex:
(InstLemma  `lsep-iff-all-sep`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x3\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index