Step * of Lemma fpf-empty-sub

[A:Type]. ∀[B,eq,g:Top].  ⊗ ⊆ g
BY
(BasicUniformUnivCD Auto⋅ THEN RepUR ``fpf-sub fpf-empty fpf-dom`` THEN Auto) }


Latex:


\mforall{}[A:Type].  \mforall{}[B,eq,g:Top].    \motimes{}  \msubseteq{}  g


By

(BasicUniformUnivCD  Auto\mcdot{}  THEN  RepUR  ``fpf-sub  fpf-empty  fpf-dom``  0  THEN  Auto)




Home Index