consider x being strict SubAlgebra of U0;
x in Sub U0 by Def15;
hence not Sub U0 is empty ; :: thesis: verum