[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