---

Step * of Lemma sep-if-all-lsep

∀g:EuclideanPlane. ∀a,b,c:Point.  (a # bc ⇒ (∀x:Point. (Colinear(x;b;c) ⇒ a ≠ x)))
BY
{ EAuto 1 }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. x : Point
7. Colinear(x;b;c)
⊢ a ≠ x

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  (\mforall{}x:Point.  (Colinear(x;b;c)  {}\mRightarrow{}  a  \mneq{}  x)))


By

---

Latex:
EAuto  1

---

Home Index