---

Step * 1 of Lemma geo-lt-angle-symm2

.....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
BY
{ ((Unfold `geo-lt-angle` -1 THEN ExRepD) THEN InstLemma `geo-cong-angle-symm` [⌜g⌝;⌜a⌝;⌜b⌝;⌜c⌝]⋅ THEN EAuto 1) }

---

Latex:

---

Latex:
.....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
\mvdash{}  abc  \mcong{}\msuba{}  cba


By

---

Latex:
((Unfold  `geo-lt-angle`  -1  THEN  ExRepD)
  THEN  InstLemma  `geo-cong-angle-symm`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{}]\mcdot{}
  THEN  EAuto  1)

---

Home Index