---

Step * of Lemma ext-family-iff

∀[P:Type]. ∀[F,G:P ⟶ Type].  uiff(F ≡ G;F ⊆ G ∧ G ⊆ F)
BY
{ (RepUR ``ext-family sub-family ext-eq`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[F,G:P  {}\mrightarrow{}  Type].    uiff(F  \mequiv{}  G;F  \msubseteq{}  G  \mwedge{}  G  \msubseteq{}  F)


By

---

Latex:
(RepUR  ``ext-family  sub-family  ext-eq``  0  THEN  Auto)

---

Home Index