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