let I be set ; :: thesis: for A, M being ManySortedSet of
for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M
let A, M be ManySortedSet of ; :: thesis: for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M
let SF be MSSubsetFamily of M; :: thesis: SF \ A is MSSubsetFamily of M
SF \ A is ManySortedSubset of bool M

proof

SF c= bool M by PBOOLE:def 23;
then A1: SF \ A c= (bool M) \ A by PBOOLE:59;
(bool M) \ A c= bool M by PBOOLE:62;
hence SF \ A c= bool M by A1, PBOOLE:15; :: according to PBOOLE:def 23 :: thesis: verum

end;

hence SF \ A is MSSubsetFamily of M ; :: thesis: verum