consider U1 being SubAlgebra of U0;
for U2 being set st U2 in {U1} holds
U2 is SubAlgebra of U0 by TARSKI:def 1;
then reconsider U00 = {U1} as SubAlgebra-Family of U0 by Def1;
take U00 ; :: thesis: not U00 is empty
thus not U00 is empty ; :: thesis: verum