---

Step * of Lemma Dbet-iff-between

∀e:EuclideanPlane. ∀a,b,c:Point.  ((∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)) ⇒ (Dbet(e;a;b;c) ⇐⇒ a_b_c))
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
6. Dbet(e;a;b;c)
⊢ a_b_c

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. ∀A,B,C:Point.  (A # BC ⇒ |AC| < |AB| + |BC|)
6. a_b_c
⊢ Dbet(e;a;b;c)

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.
    ((\mforall{}A,B,C:Point.    (A  \#  BC  {}\mRightarrow{}  |AC|  <  |AB|  +  |BC|))  {}\mRightarrow{}  (Dbet(e;a;b;c)  \mLeftarrow{}{}\mRightarrow{}  a\_b\_c))


By

---

Latex:
Auto

---

Home Index