reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily 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
|:a:| = [0] I by Def4;
then A2: meet |:a:| = M by MSSUBFAM:41;
a c= SF by XBOOLE_1:2;
hence M in SF by A1, A2, Def8; :: according to CLOSURE2:def 9 :: thesis: verum