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