---

Step * of Lemma colinear-lsep-general

∀g:OrientedPlane. ∀a,b,c,d:Point.  (Colinear(a;b;c) ⇒ Colinear(a;b;d) ⇒ c ≠ d ⇒ (∀y:Point. (y # ab ⇒ y # cd)))
BY
{ Auto }

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. Colinear(a;b;c)
7. Colinear(a;b;d)
8. c ≠ d
9. y : Point
10. y # ab
⊢ y # cd

---

Latex:

---

Latex:
\mforall{}g:OrientedPlane.  \mforall{}a,b,c,d:Point.
    (Colinear(a;b;c)  {}\mRightarrow{}  Colinear(a;b;d)  {}\mRightarrow{}  c  \mneq{}  d  {}\mRightarrow{}  (\mforall{}y:Point.  (y  \#  ab  {}\mRightarrow{}  y  \#  cd)))


By

---

Latex:
Auto

---

Home Index