let U0 be with_const_op Universal_Algebra; for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1
let U1, U2 be strict SubAlgebra of U0; U1 /\ (U1 "\/" U2) = U1
reconsider u112 = the carrier of (U1 /\ (U1 "\/" U2)) as non empty Subset of U0 by Def7;
reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def7;
reconsider A = u1 \/ u2 as non empty Subset of U0 ;
A1:
the charact of U1 = Opers (U0,u1)
by Def7;
A2:
dom (Opers (U0,u1)) = dom the charact of U0
by Def6;
U1 "\/" U2 = GenUnivAlg A
by Def13;
then A3:
A c= the carrier of (U1 "\/" U2)
by Def12;
A4:
the carrier of U1 meets the carrier of (U1 "\/" U2)
by Th17;
then A5:
the carrier of (U1 /\ (U1 "\/" U2)) = the carrier of U1 /\ the carrier of (U1 "\/" U2)
by Def9;
then A6:
the carrier of (U1 /\ (U1 "\/" U2)) c= the carrier of U1
by XBOOLE_1:17;
the carrier of U1 c= A
by XBOOLE_1:7;
then
the carrier of U1 c= the carrier of (U1 "\/" U2)
by A3;
then A7:
the carrier of U1 c= the carrier of (U1 /\ (U1 "\/" U2))
by A5, XBOOLE_1:19;
A8:
dom (Opers (U0,u112)) = dom the charact of U0
by Def6;
A9:
for n being Nat st n in dom the charact of U0 holds
the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n
the charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112)
by A4, Def9;
then
the charact of (U1 /\ (U1 "\/" U2)) = the charact of U1
by A1, A8, A2, A9, FINSEQ_1:13;
hence
U1 /\ (U1 "\/" U2) = U1
by A7, A6, XBOOLE_0:def 10; verum