let CS be MSClosureStr of S; :: thesis: ( CS is absolutely-additive implies CS is properly-lower-bound )
assume CS is absolutely-additive ; :: thesis: CS is properly-lower-bound
then A1: the Family of CS is absolutely-additive ;
thus the Family of CS is properly-lower-bound by A1; :: according to CLOSURE1:def 11 :: thesis: verum