let I be set ; :: thesis: for M being ManySortedSet of
for SF, SG being MSSubsetFamily of M holds SF /\ SG is MSSubsetFamily of M
let M be ManySortedSet of ; :: 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 /\ SG is ManySortedSubset of bool M

proof

A1: SF c= bool M by PBOOLE:def 23;
SG c= bool M by PBOOLE:def 23;
then SF /\ SG c= (bool M) /\ (bool M) by A1, PBOOLE:23;
hence SF /\ SG c= bool M ; :: according to PBOOLE:def 23 :: thesis: verum

end;

hence SF /\ SG is MSSubsetFamily of M ; :: thesis: verum