---

Step * of Lemma lsep-colinear-sep

∀g:OrientedPlane. ∀a,b,c:Point.  (a # bc ⇒ (∀y:Point. (Colinear(y;b;c) ⇒ a ≠ y)))
BY
{ (Auto THEN (InstLemma `geo-sep-or` [⌜g⌝;⌜c⌝;⌜b⌝;⌜y⌝]⋅ THENA Auto) THEN D -1) }

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index