let U0 be strict with_const_op Universal_Algebra; :: thesis: for U1 being SubAlgebra of U0
for H being Subset of U0 st H = the carrier of U0 holds
(GenUnivAlg H) "\/" U1 = GenUnivAlg H
let U1 be SubAlgebra of U0; :: thesis: for H being Subset of U0 st H = the carrier of U0 holds
(GenUnivAlg H) "\/" U1 = GenUnivAlg H
let H be Subset of U0; :: thesis: ( H = the carrier of U0 implies (GenUnivAlg H) "\/" U1 = GenUnivAlg H )
assume H = the carrier of U0 ; :: thesis: (GenUnivAlg H) "\/" U1 = GenUnivAlg H
then H \/ the carrier of U1 = H by Th3, XBOOLE_1:12;
hence (GenUnivAlg H) "\/" U1 = GenUnivAlg H by UNIALG_2:20; :: thesis: verum