Sub U0 is SubAlgebra-Family of U0

proof

hence
Sub U0 is non empty SubAlgebra-Family of U0
; :: thesis: verum
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;assume U1 in Sub U0 ; :: thesis: U1 is SubAlgebra of U0

hence U1 is SubAlgebra of U0 by UNIALG_2:def 14; :: thesis: verum