---

Step * of Lemma geo-lt-angle-symm2

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

1
.....antecedent..... 
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. abc < def
⊢ abc ≅a cba

---

Latex:

---

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


By

---

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

---

Home Index