EmptyMS I c= bool M by PBOOLE:43;
then reconsider a = EmptyMS I as MSSubsetFamily of M by PBOOLE:def 18;
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
( meet a = M & EmptyMS I c= SF ) by Th41, PBOOLE:43;
hence M in SF by A1; :: according to MSSUBFAM:def 6 :: thesis: verum