let SF be MSSubsetFamily of M; :: thesis: ( SF is absolutely-multiplicative implies SF is properly-upper-bound )
assume A1: SF is absolutely-multiplicative ; :: thesis: SF is properly-upper-bound
[0] I c= bool M by PBOOLE:49;
then reconsider a = [0] I as MSSubsetFamily of M by PBOOLE:def 23;
A2: meet a = M by Th41;
[0] I c= SF by PBOOLE:49;
hence M in SF by A1, A2, Def6; :: according to MSSUBFAM:def 7 :: thesis: verum