let CS be ClosureStr of S; :: thesis: ( CS is absolutely-additive implies CS is additive )
assume CS is absolutely-additive ; :: thesis: CS is additive
then A1: the Family of CS is absolutely-additive ;
thus the Family of CS is additive by A1; :: according to CLOSURE2:def 16 :: thesis: verum