---

Step * of Lemma geo-le-sep

∀e:BasicGeometry. ∀A,B,C,P:Point.  (|AB| ≤ |CP| ⇒ A ≠ B ⇒ C ≠ P)
BY
{ (Auto THEN (RWO "geo-le-iff" (-2) THENA Auto)) }

1
1. e : BasicGeometry
2. A : Point
3. B : Point
4. C : Point
5. P : Point
6. CP ≥ AB
7. A ≠ B
⊢ C ≠ P

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}A,B,C,P:Point.    (|AB|  \mleq{}  |CP|  {}\mRightarrow{}  A  \mneq{}  B  {}\mRightarrow{}  C  \mneq{}  P)


By

---

Latex:
(Auto  THEN  (RWO  "geo-le-iff"  (-2)  THENA  Auto))

---

Home Index