-\[\eqn{Foreign Contents:}{
- \bigforall_{C \text{ s.t. } \patchof{C} = \bot}
- D \le C \implies \patchof{D} = \bot
+\[\eqn{Foreign Inclusion}{
+ \bigforall_{D \in \foreign} D \isin C \equiv D \leq C
+}\]
+\[\eqn{Foreign Contents}{
+ \bigforall_{C \in \foreign}
+ D \le C \implies \isforeign{D}