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

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