---

Step * of Lemma sub-family_transitivity

∀[P:Type]. ∀[F,G,H:P ⟶ Type].  (F ⊆ H) supposing (F ⊆ G and G ⊆ H)
BY
{ (Unfold `sub-family` 0 THEN Auto THEN UseTrans ⌜G p⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[F,G,H:P  {}\mrightarrow{}  Type].    (F  \msubseteq{}  H)  supposing  (F  \msubseteq{}  G  and  G  \msubseteq{}  H)


By

---

Latex:
(Unfold  `sub-family`  0  THEN  Auto  THEN  UseTrans  \mkleeneopen{}G  p\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index