---

Step * of Lemma geo-tar-opp-side-mid1

∀e:HeytingGeometry. ∀a,c,r,m:Point.
  (geo-tar-opp-side(e;a;c;r;m) ⇒ a=m=c ⇒ (∀b:Point. (r-a-b ⇒ geo-tar-opp-side(e;b;c;r;m))))
BY
{ (Auto THEN (Unfold `geo-tar-opp-side` 0 THEN Unfold `geo-tar-opp-side` 6) THEN Auto) }

1
1. e : HeytingGeometry
2. a : Point
3. c : Point
4. r : Point
5. m : Point
6. a # rm
7. c # rm
8. ∃t:Point. (Colinear(r;m;t) ∧ a_t_c)
9. a=m=c
10. b : Point
11. r-a-b
12. b # rm
13. c # rm
⊢ ∃t:Point. (Colinear(r;m;t) ∧ b_t_c)

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,c,r,m:Point.
    (geo-tar-opp-side(e;a;c;r;m)  {}\mRightarrow{}  a=m=c  {}\mRightarrow{}  (\mforall{}b:Point.  (r-a-b  {}\mRightarrow{}  geo-tar-opp-side(e;b;c;r;m))))


By

---

Latex:
(Auto  THEN  (Unfold  `geo-tar-opp-side`  0  THEN  Unfold  `geo-tar-opp-side`  6)  THEN  Auto)

---

Home Index