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 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

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

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 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

proof

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

.= o0 /. u112 by A8, A10, Def6

.= o0 /. u1 by A7, A6, XBOOLE_0:def 10

.= (Opers (U0,u1)) . n by A2, A10, Def6

.= the charact of U1 . n by Def7 ; :: thesis: verum

end;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, Def9

.= o0 /. u112 by A8, A10, Def6

.= o0 /. u1 by A7, A6, XBOOLE_0:def 10

.= (Opers (U0,u1)) . n by A2, A10, Def6

.= the charact of U1 . n by Def7 ; :: thesis: verum

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