---

Step * of Lemma isect-subtype-2

∀[G:Type ⟶ Type]. ∀[A,B:Type]. ∀[F:G[A] ⟶ G[B] ⟶ Type]. ∀[X:G[A]]. ∀[Y:G[B]].
  ((⋂X:G[A]. ⋂Y:G[B].  F[X;Y]) ⊆r F[X;Y])
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[G:Type  {}\mrightarrow{}  Type].  \mforall{}[A,B:Type].  \mforall{}[F:G[A]  {}\mrightarrow{}  G[B]  {}\mrightarrow{}  Type].  \mforall{}[X:G[A]].  \mforall{}[Y:G[B]].
    ((\mcap{}X:G[A].  \mcap{}Y:G[B].    F[X;Y])  \msubseteq{}r  F[X;Y])


By

---

Latex:
Auto

---

Home Index