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