---

Step * of Lemma geo-congruence-identity3

∀[e:BasicGeometry]. ∀[a,b,c,d:Point].  (a ≡ b) supposing (cd ≅ ab and c ≡ d)
BY
{ (InstLemma `geo-congruence-identity2` [] THEN RepeatFor 7 (ParallelLast')) }

1
.....antecedent..... 
1. e : BasicGeometry
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. c ≡ d
7. cd ≅ ab
⊢ ab ≅ cd

---

Latex:

---

Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[a,b,c,d:Point].    (a  \mequiv{}  b)  supposing  (cd  \00D0  ab  and  c  \mequiv{}  d)


By

---

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

---

Home Index