---

Step * of Lemma eu-eq_dist-axiomsB

No Annotations
∀g:EuclideanPlane. ((∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)) ⇒ dist-axiomsB(g))
BY
{ ((Auto THEN Unfold `dist-axiomsB` 0) THEN (GenRepD THENA Auto)) }

1
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;c)
8. Dbet(g;a;c;d)
⊢ Dbet(g;b;c;d)

2
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;d)
8. Dbet(g;b;c;d)
⊢ Dbet(g;a;c;d)

3
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dsep(g;b;c)
8. Dbet(g;a;b;c)
9. Dbet(g;b;c;d)
⊢ Dbet(g;a;b;d)

4
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. Dbet(g;a;b;c)
7. Dsep(g;b;c)
⊢ D(a;c;c;c;a;b)

5
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. Dbet(g;a;b;c)
8. Dbet(g;a;b;d)
9. Dsep(g;a;b)
10. Dsep(g;c;d)
⊢ Dbet(g;a;c;d) ∨ Dbet(g;a;d;c)

6
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. e : Point
8. Dbet(g;a;b;c)
9. D(a;b;b;c;d;e)
⊢ D(a;c;c;c;d;e)

7
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. d : Point
7. e : Point
8. Dbet(g;a;b;c)
9. D(a;c;c;c;d;e)
⊢ D(a;b;b;c;d;e)

8
1. g : EuclideanPlane
2. ∀a,b,c:Point.  (a # bc ⇒ |ac| < |ab| + |bc|)
3. a : Point
4. b : Point
5. c : Point
6. x : Point
7. Dtri(g;a;b;c)
⊢ Dsep(g;c;x) ∨ Dtri(g;a;b;x)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanPlane.  ((\mforall{}a,b,c:Point.    (a  \#  bc  {}\mRightarrow{}  |ac|  <  |ab|  +  |bc|))  {}\mRightarrow{}  dist-axiomsB(g))


By

---

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

---

Home Index