---

Step * of Lemma lsep-iff-all-sep

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

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

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index