set a = the non-empty many-sorted over S;
take MSFull the non-empty many-sorted over S ; :: thesis: ( MSFull the non-empty many-sorted over S is strict & MSFull the non-empty many-sorted over S is non-empty & MSFull the non-empty many-sorted over S is additive & MSFull the non-empty many-sorted over S is absolutely-additive & MSFull the non-empty many-sorted over S is multiplicative & MSFull the non-empty many-sorted over S is absolutely-multiplicative & MSFull the non-empty many-sorted over S is properly-upper-bound & MSFull the non-empty many-sorted over S is properly-lower-bound )
thus ( MSFull the non-empty many-sorted over S is strict & MSFull the non-empty many-sorted over S is non-empty & MSFull the non-empty many-sorted over S is additive & MSFull the non-empty many-sorted over S is absolutely-additive & MSFull the non-empty many-sorted over S is multiplicative & MSFull the non-empty many-sorted over S is absolutely-multiplicative & MSFull the non-empty many-sorted over S is properly-upper-bound & MSFull the non-empty many-sorted over S is properly-lower-bound ) ; :: thesis: verum