---

Step * of Lemma geo-congruence-identity-sym

∀[e:EuclideanPlane]. ∀[a,b,c:Point].  a ≡ b supposing ab ≅ cc
BY
{ (Auto THEN Assert ⌜cc ≅ ab⌝⋅) }

1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab ≅ cc
⊢ cc ≅ ab

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ab ≅ cc
6. cc ≅ ab
⊢ a ≡ b

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[a,b,c:Point].    a  \mequiv{}  b  supposing  ab  \00D0  cc


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}cc  \00D0  ab\mkleeneclose{}\mcdot{})

---

Home Index