---

Step * of Lemma straight-angles-not-lt2

∀g:EuclideanPlane. ∀a,b,c,x,y,z:Point.  (a-b-c ⇒ (¬abc < xyz))
BY
{ ((Auto THEN (D 0 THENA Auto))
   THEN (Unfold `geo-lt-angle` -1 THEN D 8 THEN ExRepD)
   THEN InstLemma `angle-cong-preserves-straight-angle` [⌜g⌝;⌜x⌝;⌜y⌝;⌜p⌝;⌜a⌝;⌜b⌝;⌜c⌝] ⋅
   THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,x,y,z:Point.    (a-b-c  {}\mRightarrow{}  (\mneg{}abc  <  xyz))


By

---

Latex:
((Auto  THEN  (D  0  THENA  Auto))
  THEN  (Unfold  `geo-lt-angle`  -1  THEN  D  8  THEN  ExRepD)
  THEN  InstLemma  `angle-cong-preserves-straight-angle`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]  \mcdot{}
  THEN  EAuto  1)

---

Home Index