Sub U0 is SubAlgebra-Family of U0
proof
let U1 be set ; :: according to UNIALG_3:def 1 :: thesis: ( U1 in Sub U0 implies U1 is SubAlgebra of U0 )
assume U1 in Sub U0 ; :: thesis: U1 is SubAlgebra of U0
hence U1 is SubAlgebra of U0 by UNIALG_2:def 14; :: thesis: verum
end;
hence Sub U0 is non empty SubAlgebra-Family of U0 ; :: thesis: verum