MSAlgebra(# the Sorts of U0, the Charact of U0 #) is MSSubAlgebra of U0 by Lm1;
hence ex b₁ being MSSubAlgebra of U0 st b₁ is strict ; :: thesis: verum