---

Step * of Lemma isect-subtype-1

∀[F:Type ⟶ Type]. ∀[A:Type].  ((⋂A:Type. F[A]) ⊆r F[A])
BY
{ (Auto THEN D 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  \mforall{}[A:Type].    ((\mcap{}A:Type.  F[A])  \msubseteq{}r  F[A])


By

---

Latex:
(Auto  THEN  D  0  THEN  Auto)

---

Home Index