---

Step * of Lemma eu-congruent-between-implies-equal

∀e:EuclideanPlane. ∀[a,b,c,x:Point].  (b = x ∈ Point) supposing (a_b_c and ab=ax and bc=xc)
BY
{ (Auto THEN EuContradiction THEN (Assert ¬(a = b ∈ Point) BY (ParallelLast THEN Eliminate ⌜a⌝⋅ THEN Auto))) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. x : Point
6. bc=xc
7. ab=ax
8. a_b_c
9. ¬(b = x ∈ Point)
10. ¬(a = b ∈ Point)
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b,c,x:Point].    (b  =  x)  supposing  (a\_b\_c  and  ab=ax  and  bc=xc)


By

---

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

---

Home Index