set U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #);
the Sorts of U0 is OrderSortedSet of S by OSALG_1:17;
then reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict OSSubAlgebra of U0 by MSUALG_2:37, OSALG_1:17;
take U1 ; :: thesis: ( U1 is non-empty & U1 is strict )
thus ( U1 is non-empty & U1 is strict ) ; :: thesis: verum