Step
*
of Lemma
null-class-is-empty
∀[es,e:Top].  (Null es e ~ {})
BY
{ (Auto THEN RepUR ``null-class`` 0 THEN Auto) }
Latex:
Latex:
\mforall{}[es,e:Top].    (Null  es  e  \msim{}  \{\})
By
Latex:
(Auto  THEN  RepUR  ``null-class``  0  THEN  Auto)
Home
Index