take {} ; :: thesis: for U1 being set st U1 in {} holds
U1 is SubAlgebra of U0
thus for U1 being set st U1 in {} holds
U1 is SubAlgebra of U0 ; :: thesis: verum