[[0]] I c= bool M by PBOOLE:49;
then reconsider a = [[0]] I as MSSubsetFamily of M by PBOOLE:def 23;
let SF be MSSubsetFamily 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
( union a = [[0]] I & [[0]] I c= SF ) by MBOOLEAN:22, PBOOLE:49;
hence [[0]] I in SF by A1, Def4; :: according to MSSUBFAM:def 8 :: thesis: verum