thus MSFull MS is strict ; :: thesis: ( MSFull MS is additive & MSFull MS is absolutely-additive & MSFull MS is multiplicative & MSFull MS is absolutely-multiplicative & MSFull MS is properly-upper-bound & MSFull MS is properly-lower-bound )
thus ( the Family of (MSFull MS) is additive & the Family of (MSFull MS) is absolutely-additive & the Family of (MSFull MS) is multiplicative & the Family of (MSFull MS) is absolutely-multiplicative & the Family of (MSFull MS) is properly-upper-bound & the Family of (MSFull MS) is properly-lower-bound ) ; :: according to CLOSURE1:def 5,CLOSURE1:def 6,CLOSURE1:def 7,CLOSURE1:def 8,CLOSURE1:def 9,CLOSURE1:def 10 :: thesis: verum