---

Step * of Lemma Dcong-iff-cong

∀g:EuclideanPlane. ∀a,b,c,d:Point.  (Dcong(g;a;b;c;d) ⇐⇒ ab ≅ cd)
BY
{ Auto }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. Dcong(g;a;b;c;d)
⊢ ab ≅ cd

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≅ cd
⊢ Dcong(g;a;b;c;d)

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (Dcong(g;a;b;c;d)  \mLeftarrow{}{}\mRightarrow{}  ab  \mcong{}  cd)


By

---

Latex:
Auto

---

Home Index