let I be set ; :: thesis: for A, M being ManySortedSet of I
for SF being MSSubsetFamily of M holds SF \ A is MSSubsetFamily of M
let A, M be ManySortedSet of I; :: 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 c= bool M by PBOOLE:def 18;
then A1: SF \ A c= (bool M) \ A by PBOOLE:53;
(bool M) \ A c= bool M by PBOOLE:56;
then SF \ A c= bool M by A1, PBOOLE:13;
hence SF \ A is MSSubsetFamily of M by PBOOLE:def 18; :: thesis: verum