let I be set ; :: thesis: for M being ManySortedSet of I
for SF, SG being MSSubsetFamily of M holds SF (/\) SG is MSSubsetFamily of M
let M be ManySortedSet of I; :: thesis: for SF, SG being MSSubsetFamily of M holds SF (/\) SG is MSSubsetFamily of M
let SF, SG be MSSubsetFamily of M; :: thesis: SF (/\) SG is MSSubsetFamily of M
( SF c= bool M & SG c= bool M ) by PBOOLE:def 18;
then SF (/\) SG c= (bool M) (/\) (bool M) by PBOOLE:21;
hence SF (/\) SG is MSSubsetFamily of M by PBOOLE:def 18; :: thesis: verum