---

Step * of Lemma erected-perp-opp-side-triangle

∀e:HeytingGeometry. ∀a,b,c,p,t:Point.
  ((c # ba ∧ ((ab ⊥ pa ∧ Colinear(a;b;t)) ∧ p-t-c) ∧ p # ba) ⇒ geo-tar-opp-side(e;p;c;a;b))
BY
{ (Auto THEN ((Assert c # ab BY Auto) THEN (Assert p # ab BY Auto)) THEN Unfold `geo-tar-opp-side` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:HeytingGeometry.  \mforall{}a,b,c,p,t:Point.
    ((c  \#  ba  \mwedge{}  ((ab  \mbot{}  pa  \mwedge{}  Colinear(a;b;t))  \mwedge{}  p-t-c)  \mwedge{}  p  \#  ba)  {}\mRightarrow{}  geo-tar-opp-side(e;p;c;a;b))


By

---

Latex:
(Auto
  THEN  ((Assert  c  \#  ab  BY  Auto)  THEN  (Assert  p  \#  ab  BY  Auto))
  THEN  Unfold  `geo-tar-opp-side`  0
  THEN  Auto)

---

Home Index