scheme :: CLOSURE1:sch 1
MSSUBSET{ F₁() -> set , F₂() -> non-empty ManySortedSet of F₁(), F₃() -> ManySortedSet of F₁(), P₁[ set ] } :

( ( for X being ManySortedSet of F₁() holds
( X in F₂() iff ( X in F₃() & P₁[X] ) ) ) implies F₂() c= F₃() )