---

Step * of Lemma not-lt-zero-angle

∀e:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (abc < xyz ⇒ (y_z_x ∨ y_x_z) ⇒ False)
BY
{ (((Auto THEN Unfold `geo-lt-angle` -2) THEN ExRepD) THEN Assert ⌜out(y xz)⌝⋅ THEN Auto THEN D -1 THEN EAuto 2) }

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (abc  <  xyz  {}\mRightarrow{}  (y\_z\_x  \mvee{}  y\_x\_z)  {}\mRightarrow{}  False)


By

---

Latex:
(((Auto  THEN  Unfold  `geo-lt-angle`  -2)  THEN  ExRepD)
  THEN  Assert  \mkleeneopen{}out(y  xz)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  EAuto  2)

---

Home Index