---

Step * of Lemma geo-lt-angle-symm

∀g:EuclideanPlane. ∀a,b,c,d,e,f:Point.  (abc < def ⇒ d # ef ⇒ abc < fed)
BY
{ (Auto THEN InstLemma `geo-cong-angle-preserves-lt-angle2` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝;⌜f⌝;⌜e⌝;⌜d⌝;⌜d⌝;⌜e⌝;⌜f⌝]⋅ THEN EAuto 2) }

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d,e,f:Point.    (abc  <  def  {}\mRightarrow{}  d  \#  ef  {}\mRightarrow{}  abc  <  fed)


By

---

Latex:
(Auto
  THEN  InstLemma  `geo-cong-angle-preserves-lt-angle2`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}
  THEN  EAuto  2)

---

Home Index