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:| = [[0]] I by Def4;
then A2: union |:a:| = [[0]] I by MBOOLEAN:22;
a c= SF by XBOOLE_1:2;
hence [[0]] I in SF by A1, A2, Def6; :: according to CLOSURE2:def 10 :: thesis: verum