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 23;
then A1: SF \ A c= (bool M) \ A by PBOOLE:59;
(bool M) \ A c= bool M by PBOOLE:62;
then SF \ A c= bool M by A1, PBOOLE:15;
hence SF \ A is MSSubsetFamily of M by PBOOLE:def 23; :: thesis: verum