let U0 be Universal_Algebra; :: thesis: for U1 being SubAlgebra of U0
for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds
(GenUnivAlg A) "\/" U1 = GenUnivAlg B
let U1 be SubAlgebra of U0; :: thesis: for A, B being Subset of U0 st ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 holds
(GenUnivAlg A) "\/" U1 = GenUnivAlg B
let A, B be Subset of U0; :: thesis: ( ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 implies (GenUnivAlg A) "\/" U1 = GenUnivAlg B )
reconsider u1 = the carrier of U1, a = the carrier of (GenUnivAlg A) as non empty Subset of U0 by Def7;
assume that
A1: ( A <> {} or Constants U0 <> {} ) and
A2: B = A \/ the carrier of U1 ; :: thesis: (GenUnivAlg A) "\/" U1 = GenUnivAlg B
A3: A c= the carrier of (GenUnivAlg A) by Def12;
A4: B c= the carrier of (GenUnivAlg B) by Def12;
A c= B by A2, XBOOLE_1:7;
then A5: A c= the carrier of (GenUnivAlg B) by A4;

now :: thesis: ( ( A <> {} & the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} ) or ( Constants U0 <> {} & the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} ) )

per cases ( A <> {} or Constants U0 <> {} ) by A1;

case A <> {} ; :: thesis: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {}

hence the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} by A3, A5, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum

end;

case A6: Constants U0 <> {} ; :: thesis: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {}

( Constants U0 is Subset of (GenUnivAlg A) & Constants U0 is Subset of (GenUnivAlg B) ) by Th15;
hence the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} by A6, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum

end;

end;

end;

then the carrier of (GenUnivAlg A) meets the carrier of (GenUnivAlg B) ;
then A7: the carrier of ((GenUnivAlg A) /\ (GenUnivAlg B)) = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by Def9;
reconsider b = a \/ u1 as non empty Subset of U0 ;
A8: the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) c= a by XBOOLE_1:17;
A c= the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A3, A5, XBOOLE_1:19;
then GenUnivAlg A is SubAlgebra of (GenUnivAlg A) /\ (GenUnivAlg B) by A1, A7, Def12;
then a is non empty Subset of ((GenUnivAlg A) /\ (GenUnivAlg B)) by Def7;
then a = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A7, A8;
then A9: a c= the carrier of (GenUnivAlg B) by XBOOLE_1:17;
u1 c= B by A2, XBOOLE_1:7;
then u1 c= the carrier of (GenUnivAlg B) by A4;
then b c= the carrier of (GenUnivAlg B) by A9, XBOOLE_1:8;
then A10: GenUnivAlg b is strict SubAlgebra of GenUnivAlg B by Def12;
A11: (GenUnivAlg A) "\/" U1 = GenUnivAlg b by Def13;
then A12: a \/ u1 c= the carrier of ((GenUnivAlg A) "\/" U1) by Def12;
A \/ u1 c= a \/ u1 by A3, XBOOLE_1:13;
then B c= the carrier of ((GenUnivAlg A) "\/" U1) by A2, A12;
then GenUnivAlg B is strict SubAlgebra of (GenUnivAlg A) "\/" U1 by A2, Def12;
hence (GenUnivAlg A) "\/" U1 = GenUnivAlg B by A11, A10, Th10; :: thesis: verum