---

Step * of Lemma colinear-lsep'

∀g:OrientedPlane. ∀a,b,c,y:Point.  (y # ab ⇒ b ≠ c ⇒ Colinear(a;b;c) ⇒ y # cb)
BY
{ (Auto THEN (InstLemma `colinear-lsep` [⌜g⌝;⌜a⌝;⌜b⌝;⌜y⌝;⌜c⌝]⋅ THENA Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `colinear-lsep`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index