---

Step * of Lemma colinear-lsep-alt

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

1
1. g : OrientedPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. z : Point
7. a # bc
8. x ≠ b
9. Colinear(a;b;x)
10. z ≠ c
11. Colinear(x;c;z)
12. x # bc
⊢ z # bc

---

Latex:

---

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


By

---

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

---

Home Index