let CS be ClosureStr of S; :: thesis: ( CS is absolutely-multiplicative implies CS is properly-upper-bound )
assume CS is absolutely-multiplicative ; :: thesis: CS is properly-upper-bound
then A1: the Family of CS is absolutely-multiplicative ;
thus the Family of CS is properly-upper-bound by A1; :: according to CLOSURE2:def 20 :: thesis: verum