set x = the strict SubAlgebra of U0;
the strict SubAlgebra of U0 in Sub U0 by Def15;
hence not Sub U0 is empty ; :: thesis: verum