---

Step * of Lemma geo-out-strict_weakening

∀e:BasicGeometry. ∀a,b,c:Point.  (Colinear(a;b;c) ⇒ (¬c_a_b) ⇒ a ≠ b ⇒ b ≠ c ⇒ geo-out-strict(e;a;b;c))
BY
{ (((Auto THEN D 0) THENA Auto) THEN D -1) }

1
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. Colinear(a;b;c)
6. ¬c_a_b
7. a ≠ b
8. b ≠ c
9. ¬a-b-c
10. ¬a-c-b
⊢ False

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}a,b,c:Point.
    (Colinear(a;b;c)  {}\mRightarrow{}  (\mneg{}c\_a\_b)  {}\mRightarrow{}  a  \mneq{}  b  {}\mRightarrow{}  b  \mneq{}  c  {}\mRightarrow{}  geo-out-strict(e;a;b;c))


By

---

Latex:
(((Auto  THEN  D  0)  THENA  Auto)  THEN  D  -1)

---

Home Index