set x = the strict MSSubAlgebra of U0;
the strict MSSubAlgebra of U0 in MSSub U0 by Def19;
hence not MSSub U0 is empty ; :: thesis: verum