let CS be MSClosureStr of S; :: thesis: ( CS is absolutely-additive implies CS is additive )
assume CS is absolutely-additive ; :: thesis: CS is additive
hence the Family of CS is additive ; :: according to CLOSURE1:def 6 :: thesis: verum