reconsider a = {} as SubsetFamily of M by XBOOLE_1:2;
let SF be SubsetFamily of M; :: thesis: ( SF is absolutely-additive implies SF is properly-lower-bound )
assume A1: SF is absolutely-additive ; :: thesis: SF is properly-lower-bound
|:a:| = EmptyMS I ;
then A2: union |:a:| = EmptyMS I by MBOOLEAN:21;
a c= SF ;
hence EmptyMS I in SF by A1, A2; :: according to CLOSURE2:def 9 :: thesis: verum