---

Step * of Lemma hp-angles-not-lt-and-cong

∀e:EuclideanPlane. ∀a,b,c,d:Point.  ((abc ≅ρ dbc ∧ half-plane-lt-angle(e;d;a;b;c)) ⇒ False)
BY
{ ((((Auto THEN D -1) THEN D 6) THEN Auto) THEN FLemma `left-not-colinear` [11] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    ((abc  \00D0\mrho{}  dbc  \mwedge{}  half-plane-lt-angle(e;d;a;b;c))  {}\mRightarrow{}  False)


By

---

Latex:
((((Auto  THEN  D  -1)  THEN  D  6)  THEN  Auto)  THEN  FLemma  `left-not-colinear`  [11]  THEN  Auto)

---

Home Index