consider a being non-empty many-sorted of S;
take MSFull a ; :: thesis: ( MSFull a is strict & MSFull a is non-empty & MSFull a is additive & MSFull a is absolutely-additive & MSFull a is multiplicative & MSFull a is absolutely-multiplicative & MSFull a is properly-upper-bound & MSFull a is properly-lower-bound )
thus ( MSFull a is strict & MSFull a is non-empty & MSFull a is additive & MSFull a is absolutely-additive & MSFull a is multiplicative & MSFull a is absolutely-multiplicative & MSFull a is properly-upper-bound & MSFull a is properly-lower-bound ) ; :: thesis: verum