---

Step * of Lemma eu-eq_dist-axiomsA

No Annotations
∀g:EuclideanPlane. dist-axiomsA(g)
BY
{ ((Auto THEN Unfold `dist-axiomsA` 0) THEN (GenRepD THENA Auto)) }

1
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. h : Point
9. D(a;b;c;d;e;f)
⊢ D(a;b;c;d;h;h)

2
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. D(a;b;c;c;e;f)
⊢ D(a;b;d;d;e;f)

3
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. D(a;b;c;d;e;f)
⊢ D(b;a;c;d;e;f)

4
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. D(a;b;c;d;e;f)
⊢ D(a;b;c;d;f;e)

5
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. D(a;b;c;d;e;f)
⊢ D(c;d;a;b;e;f)

6
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)

7
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. D(a;b;c;d;e;f)
11. ¬D(x;y;y;y;e;f)
⊢ D(a;b;c;d;x;y)

8
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. x : Point
9. y : Point
10. D(a;b;c;d;e;f)
11. ¬D(a;b;b;b;x;y)
⊢ D(x;y;c;d;e;f)

9
1. g : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. e : Point
7. f : Point
8. D(a;b;b;b;c;d)
⊢ D(a;b;b;b;e;f) ∨ D(e;f;f;f;c;d)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  dist-axiomsA(g)


By

---

Latex:
((Auto  THEN  Unfold  `dist-axiomsA`  0)  THEN  (GenRepD  THENA  Auto))

---

Home Index