---

Step * of Lemma geo-triangle-separation

∀e:HeytingGeometry. ∀a,b,c:Point.
  (a # bc
  ⇒ {∀x,y:Point.  (((Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x ≠ b ∧ y ≠ b) ⇒ (x # by ∧ (∀m:Point. (x-m-y ⇒ m ≠ b))))})
BY
{ (Auto THEN (FLemma `geo-triangle-implies` [-1] THENA Auto) THEN SplitAndHyps THEN RepeatFor 3 ((D 0 THENA Auto))) }

1
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. a # bc
6. c # ba
7. c # ab
8. a ≠ c
9. ¬a_b_c
10. ∀z:Point. (z ≠ b ⇒ Colinear(a;b;z) ⇒ z # bc)
11. x : Point
12. y : Point
13. (Colinear(a;b;x) ∧ Colinear(c;b;y)) ∧ x ≠ b ∧ y ≠ b
⊢ x # by ∧ (∀m:Point. (x-m-y ⇒ m ≠ b))

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c:Point.
    (a  \#  bc
    {}\mRightarrow{}  \{\mforall{}x,y:Point.
                (((Colinear(a;b;x)  \mwedge{}  Colinear(c;b;y))  \mwedge{}  x  \mneq{}  b  \mwedge{}  y  \mneq{}  b)
                {}\mRightarrow{}  (x  \#  by  \mwedge{}  (\mforall{}m:Point.  (x-m-y  {}\mRightarrow{}  m  \mneq{}  b))))\})


By

---

Latex:
(Auto
  THEN  (FLemma  `geo-triangle-implies`  [-1]  THENA  Auto)
  THEN  SplitAndHyps
  THEN  RepeatFor  3  ((D  0  THENA  Auto)))

---

Home Index