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