---

Step * 1 of Lemma geo-congruent-full-symmetry


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}
BY
{ (Unfold `guard` 0 THEN EAuto 1) }

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

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  ab  \mcong{}  cd
\mvdash{}  \{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\}


By

---

Latex:
(Unfold  `guard`  0  THEN  EAuto  1)

---

Home Index