consider x being strict MSSubAlgebra of U0;
x in MSSub U0 by Def20;
hence not MSSub U0 is empty ; :: thesis: verum