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
() "\/" 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
() "\/" U1 = GenUnivAlg B

let A, B be Subset of U0; :: thesis: ( ( A <> {} or Constants U0 <> {} ) & B = A \/ the carrier of U1 implies () "\/" U1 = GenUnivAlg B )
reconsider u1 = the carrier of U1, a = the carrier of () as non empty Subset of U0 by Def7;
assume that
A1: ( A <> {} or Constants U0 <> {} ) and
A2: B = A \/ the carrier of U1 ; :: thesis: () "\/" U1 = GenUnivAlg B
A3: A c= the carrier of () by Def12;
A4: B c= the carrier of () by Def12;
A c= B by ;
then A5: A c= the carrier of () by A4;
now :: thesis: ( ( A <> {} & the carrier of () /\ the carrier of () <> {} ) or ( Constants U0 <> {} & the carrier of () /\ the carrier of () <> {} ) )
per cases ( A <> {} or Constants U0 <> {} ) by A1;
case A <> {} ; :: thesis: the carrier of () /\ the carrier of () <> {}
hence the carrier of () /\ the carrier of () <> {} by ; :: thesis: verum
end;
case A6: Constants U0 <> {} ; :: thesis: the carrier of () /\ the carrier of () <> {}
( Constants U0 is Subset of () & Constants U0 is Subset of () ) by Th15;
hence the carrier of () /\ the carrier of () <> {} by ; :: thesis: verum
end;
end;
end;
then the carrier of () meets the carrier of () ;
then A7: the carrier of (() /\ ()) = the carrier of () /\ the carrier of () by Def9;
reconsider b = a \/ u1 as non empty Subset of U0 ;
A8: the carrier of () /\ the carrier of () c= a by XBOOLE_1:17;
A c= the carrier of () /\ the carrier of () by ;
then GenUnivAlg A is SubAlgebra of () /\ () by ;
then a is non empty Subset of (() /\ ()) by Def7;
then a = the carrier of () /\ the carrier of () by A7, A8;
then A9: a c= the carrier of () by XBOOLE_1:17;
u1 c= B by ;
then u1 c= the carrier of () by A4;
then b c= the carrier of () by ;
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 (() "\/" U1) by Def12;
A \/ u1 c= a \/ u1 by ;
then B c= the carrier of (() "\/" U1) by ;
then GenUnivAlg B is strict SubAlgebra of () "\/" U1 by ;
hence (GenUnivAlg A) "\/" U1 = GenUnivAlg B by ; :: thesis: verum