Step
*
of Lemma
ss-sep-symmetry
∀ss:SeparationSpace. ∀x,y:Point. (x # y
⇒ y # x)
BY
{ ((D 0 THENA Auto) THEN UseWitness ⌜ss."#symm"⌝⋅ THEN RepUR ``ss-point ss-sep`` 0 THEN D 1 THEN Auto) }
Latex:
Latex:
\mforall{}ss:SeparationSpace. \mforall{}x,y:Point. (x \# y {}\mRightarrow{} y \# x)
By
Latex:
((D 0 THENA Auto) THEN UseWitness \mkleeneopen{}ss."\#symm"\mkleeneclose{}\mcdot{} THEN RepUR ``ss-point ss-sep`` 0 THEN D 1 THEN Auto)
Home
Index