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