---

Step * 1 of Lemma colinear-lsep-alt


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
BY
{ (InstLemma `colinear-lsep` [⌜g⌝;⌜x⌝;⌜c⌝;⌜b⌝;⌜z⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

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


By

---

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

---

Home Index