---

Step * of Lemma eu-congruent-trivial

∀e:EuclideanPlane. ∀[a,b:Point].  aa=bb
BY
{ (Auto THEN EuContradiction THEN Assert ⌜¬(a = b ∈ Point)⌝⋅) }

1
.....assertion..... 
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. ¬aa=bb
⊢ ¬(a = b ∈ Point)

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. ¬aa=bb
5. ¬(a = b ∈ Point)
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  EuContradiction  THEN  Assert  \mkleeneopen{}\mneg{}(a  =  b)\mkleeneclose{}\mcdot{})

---

Home Index