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