---

Step * 6 of Lemma eu-eq_dist-axiomsA


1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. D(a;b;b;b;c;d)
⊢ ¬D(c;d;d;d;a;b)
BY
{ (((Unfold `dist` -1 THEN Unfold `dist` 0) THEN ExRepD) THEN (D 0 THEN Auto) THEN ExRepD) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. a' : Point
7. b' : Point
8. c' : Point
9. u : {u:Point| c' # u} 
10. B(a'b'c')
11. B(a'uc')
12. ab ≅ a'b'
13. bb ≅ b'c'
14. cd ≅ a'u
15. a1 : Point
16. b1 : Point
17. c1 : Point
18. u1 : {u:Point| c1 # u} 
19. B(a1b1c1)
20. B(a1u1c1)
21. cd ≅ a1b1
22. dd ≅ b1c1
23. ab ≅ a1u1
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  d  :  Point
6.  D(a;b;b;b;c;d)
\mvdash{}  \mneg{}D(c;d;d;d;a;b)


By

---

Latex:
(((Unfold  `dist`  -1  THEN  Unfold  `dist`  0)  THEN  ExRepD)  THEN  (D  0  THEN  Auto)  THEN  ExRepD)

---

Home Index