---

Step * of Lemma geo-congruent-trivial

No Annotations
∀e:EuclideanPlane. ∀[a,b:Point].  aa ≅ bb
BY
{ (Auto THEN GeoContradiction THEN (gSeparatedCases ⌜a⌝ ⌜b⌝⋅ THENA Auto)) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. ¬aa ≅ bb
5. a # b
⊢ False

2
1. e : EuclideanPlane
2. b : Point
3. a : Point
4. ¬bb ≅ bb
5. a ≡ b
⊢ False

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    aa  \mcong{}  bb


By

---

Latex:
(Auto  THEN  GeoContradiction  THEN  (gSeparatedCases  \mkleeneopen{}a\mkleeneclose{}  \mkleeneopen{}b\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index