EmptyMS I c= bool M by PBOOLE:43;
then reconsider a = EmptyMS I as MSSubsetFamily of M by PBOOLE:def 18;
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 = EmptyMS I & EmptyMS I c= SF ) by PBOOLE:43;
hence EmptyMS I in SF by A1; :: according to MSSUBFAM:def 7 :: thesis: verum