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