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