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;

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

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) <> {} ) )end;

then
the carrier of (GenUnivAlg A) meets the carrier of (GenUnivAlg B)
;per cases
( A <> {} or Constants U0 <> {} )
by A1;

end;

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

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