let CS be ClosureStr of S; :: thesis: ( CS is absolutely-additive implies CS is properly-lower-bound )
assume CS is absolutely-additive ; :: thesis: CS is properly-lower-bound
hence the Family of CS is properly-lower-bound ; :: according to CLOSURE2:def 21 :: thesis: verum