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 non-empty & b₁ is strict ) ; :: thesis: verum