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 )
assume A1: ( ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 ) ; :: thesis: (GenUnivAlg A) "\/" U1 = GenUnivAlg B
then A2: A c= the carrier of (GenUnivAlg A) by Def13;
reconsider u1 = the carrier of U1, a = the carrier of (GenUnivAlg A) as non empty Subset of U0 by Def8;
reconsider b = a \/ u1 as non empty Subset of U0 ;
A3: (GenUnivAlg A) "\/" U1 = GenUnivAlg b by Def14;
then A4: a \/ u1 c= the carrier of ((GenUnivAlg A) "\/" U1) by Def13;
A \/ u1 c= a \/ u1 by A2, XBOOLE_1:13;
then B c= the carrier of ((GenUnivAlg A) "\/" U1) by A1, A4, XBOOLE_1:1;
then A5: GenUnivAlg B is strict SubAlgebra of (GenUnivAlg A) "\/" U1 by A1, Def13;
( B c= the carrier of (GenUnivAlg B) & u1 c= B & A c= B ) by A1, Def13, XBOOLE_1:7;
then A6: ( u1 c= the carrier of (GenUnivAlg B) & A c= the carrier of (GenUnivAlg B) ) by XBOOLE_1:1;
then A7: A c= the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A2, XBOOLE_1:19;

now

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 A2, A6, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum

end;

case A8: 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 Th18;
hence the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) <> {} by A8, XBOOLE_1:3, XBOOLE_1:19; :: thesis: verum

end;

end;

end;

then the carrier of (GenUnivAlg A) meets the carrier of (GenUnivAlg B) by XBOOLE_0:def 7;
then A9: the carrier of ((GenUnivAlg A) /\ (GenUnivAlg B)) = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by Def10;
then GenUnivAlg A is SubAlgebra of (GenUnivAlg A) /\ (GenUnivAlg B) by A1, A7, Def13;
then A10: a is non empty Subset of ((GenUnivAlg A) /\ (GenUnivAlg B)) by Def8;
the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) c= a by XBOOLE_1:17;
then a = the carrier of (GenUnivAlg A) /\ the carrier of (GenUnivAlg B) by A9, A10, XBOOLE_0:def 10;
then a c= the carrier of (GenUnivAlg B) by XBOOLE_1:17;
then b c= the carrier of (GenUnivAlg B) by A6, XBOOLE_1:8;
then GenUnivAlg b is strict SubAlgebra of GenUnivAlg B by Def13;
hence (GenUnivAlg A) "\/" U1 = GenUnivAlg B by A3, A5, Th13; :: thesis: verum