---

Step * of Lemma geo-gt-prim-iff-lt

No Annotations
∀e:EuclideanPlane. ∀a,b,c,d:Point.  (ab>cd ⇐⇒ |cd| < |ab|)
BY
{ Auto }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. ab>cd
⊢ |cd| < |ab|

2
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. d : Point
6. |cd| < |ab|
⊢ ab>cd

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c,d:Point.    (ab>cd  \mLeftarrow{}{}\mRightarrow{}  |cd|  <  |ab|)


By

---

Latex:
Auto

---

Home Index