let CS be MSClosureStr of S; :: thesis: ( CS is absolutely-multiplicative implies CS is properly-upper-bound )
assume CS is absolutely-multiplicative ; :: thesis: CS is properly-upper-bound
hence the Family of CS is properly-upper-bound ; :: according to CLOSURE1:def 9 :: thesis: verum