reconsider U1 = MSAlgebra(# the Sorts of U0, the Charact of U0 #) as strict MSSubAlgebra of U0 by MSUALG_2:37;
take U1 ; :: thesis: U1 is order-sorted
thus U1 is order-sorted by Th4; :: thesis: verum