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