---

Step * of Lemma fpf-empty-sub

∀[A:Type]. ∀[B,eq,g:Top].  ⊗ ⊆ g
BY
{ (BasicUniformUnivCD Auto⋅ THEN RepUR ``fpf-sub fpf-empty fpf-dom`` 0 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