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