---

Step * of Lemma eu-congruent-preserves-between

∀e:EuclideanPlane. ∀[a,b,c,a',b',c':Point].  (a'_b'_c') supposing (bc=b'c' and ac=a'c' and ab=a'b' and a_b_c)
BY
{ (Auto THEN EuContradiction) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. a' : Point
6. b' : Point
7. c' : Point
8. a_b_c
9. ab=a'b'
10. ac=a'c'
11. bc=b'c'
12. ¬a'_b'_c'
⊢ False

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  EuContradiction)

---

Home Index