---

Step * of Lemma geo-congruent-full-symmetry

No Annotations
∀e:EuclideanPlane
  ∀[a,b,c,d:Point].  {ba ≅ cd ∧ ab ≅ dc ∧ ba ≅ dc ∧ cd ≅ ab ∧ dc ≅ ab ∧ cd ≅ ba ∧ dc ≅ ba} supposing ab ≅ cd
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab ≅ cd
⊢ {ba ≅ cd ∧ ab ≅ dc ∧ ba ≅ dc ∧ cd ≅ ab ∧ dc ≅ ab ∧ cd ≅ ba ∧ dc ≅ ba}

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane
    \mforall{}[a,b,c,d:Point].
        \{ba  \mcong{}  cd  \mwedge{}  ab  \mcong{}  dc  \mwedge{}  ba  \mcong{}  dc  \mwedge{}  cd  \mcong{}  ab  \mwedge{}  dc  \mcong{}  ab  \mwedge{}  cd  \mcong{}  ba  \mwedge{}  dc  \mcong{}  ba\}  supposing  ab  \mcong{}  cd


By

---

Latex:
Auto

---

Home Index