---

Step * of Lemma Dsep-iff-sep

No Annotations
∀e:EuclideanPlane. ∀a,b:Point.  (Dsep(e;a;b) ⇐⇒ a # b)
BY
{ ((EAuto 1 THEN Unfold `dist-sep` 0)
   THEN (InstLemma `dist-iff-lt` [⌜e⌝;⌜a⌝;⌜b⌝;⌜b⌝;⌜b⌝;⌜b⌝;⌜b⌝]⋅ THEN Auto)
   THEN ((D -2 THEN Auto) THEN FLemma `geo-zero-lt-iff` [-2] THEN Auto)
   THEN Subst' |ab| + |bb| = |ab| ∈ Length 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.    (Dsep(e;a;b)  \mLeftarrow{}{}\mRightarrow{}  a  \#  b)


By

---

Latex:
((EAuto  1  THEN  Unfold  `dist-sep`  0)
  THEN  (InstLemma  `dist-iff-lt`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  ((D  -2  THEN  Auto)  THEN  FLemma  `geo-zero-lt-iff`  [-2]  THEN  Auto)
  THEN  Subst'  |ab|  +  |bb|  =  |ab|  0
  THEN  Auto)

---

Home Index