let U0 be with_const_op Universal_Algebra; :: thesis: for U1, U2 being strict SubAlgebra of U0 holds U1 /\ (U1 "\/" U2) = U1
let U1, U2 be strict SubAlgebra of U0; :: thesis: U1 /\ (U1 "\/" U2) = U1
reconsider u112 = the carrier of (U1 /\ (U1 "\/" U2)) as non empty Subset of U0 by Def8;
reconsider u1 = the carrier of U1, u2 = the carrier of U2 as non empty Subset of U0 by Def8;
reconsider A = u1 \/ u2 as non empty Subset of U0 ;
A1: the charact of U1 = Opers (U0,u1) by Def8;
A2: dom (Opers (U0,u1)) = dom the charact of U0 by Def7;
U1 "\/" U2 = GenUnivAlg A by Def14;
then A3: A c= the carrier of (U1 "\/" U2) by Def13;
A4: the carrier of U1 meets the carrier of (U1 "\/" U2) by Th20;
then A5: the carrier of (U1 /\ (U1 "\/" U2)) = the carrier of U1 /\ the carrier of (U1 "\/" U2) by Def10;
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, XBOOLE_1:1;
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 Def7;
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

proof

let n be Nat; :: thesis: ( n in dom the charact of U0 implies the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n )
assume A10: n in dom the charact of U0 ; :: thesis: the charact of (U1 /\ (U1 "\/" U2)) . n = the charact of U1 . n
then reconsider o0 = the charact of U0 . n as operation of U0 by FUNCT_1:def 3;
thus the charact of (U1 /\ (U1 "\/" U2)) . n = (Opers (U0,u112)) . n by A4, Def10
.= o0 /. u112 by A8, A10, Def7
.= o0 /. u1 by A7, A6, XBOOLE_0:def 10
.= (Opers (U0,u1)) . n by A2, A10, Def7
.= the charact of U1 . n by Def8 ; :: thesis: verum

end;

the charact of (U1 /\ (U1 "\/" U2)) = Opers (U0,u112) by A4, Def10;
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; :: thesis: verum