---

Step * of Lemma eu-congruence-identity3

∀[e:EuclideanPlane]. ∀[a,b,c,d:Point].  (a = b ∈ Point) supposing (cd=ab and (c = d ∈ Point))
BY
{ (InstLemma `eu-congruence-identity2` [] THEN RepeatFor 7 (ParallelLast')) }

1
.....antecedent..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c = d ∈ Point
7. cd=ab
⊢ ab=cd

---

Latex:

---

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[a,b,c,d:Point].    (a  =  b)  supposing  (cd=ab  and  (c  =  d))


By

---

Latex:
(InstLemma  `eu-congruence-identity2`  []  THEN  RepeatFor  7  (ParallelLast'))

---

Home Index