let I be I_Lattice; :: thesis: for FI being Filter of I holds the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
let FI be Filter of I; :: thesis: the L_join of I is BinOp of the carrier of I, equivalence_wrt FI
set R = equivalence_wrt FI;
let x1, y1, x2, y2 be Element of the carrier of I; :: according to FILTER_1:def 2 :: thesis: ( [x1,y1] in equivalence_wrt FI & [x2,y2] in equivalence_wrt FI implies [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI )
assume that
A1: [x1,y1] in equivalence_wrt FI and
A2: [x2,y2] in equivalence_wrt FI ; :: thesis: [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI
A3: x2 <=> y2 in FI by A2, FILTER_0:def 11;
then A4: x2 => y2 in FI by FILTER_0:8;
A5: x1 "/\" (x1 => y1) [= y1 by FILTER_0:def 7;
x1 "/\" ((x1 => y1) "/\" (x2 => y2)) = (x1 "/\" (x1 => y1)) "/\" (x2 => y2) by LATTICES:def 7;
then A6: x1 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 by A5, FILTER_0:2;
A7: x2 "/\" ((x1 => y1) "/\" (x2 => y2)) = (x2 "/\" (x1 => y1)) "/\" (x2 => y2) by LATTICES:def 7;
A8: x2 "/\" (x2 => y2) [= y2 by FILTER_0:def 7;
(x1 => y1) "/\" (x2 "/\" (x2 => y2)) = ((x1 => y1) "/\" x2) "/\" (x2 => y2) by LATTICES:def 7;
then x2 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y2 by A7, A8, FILTER_0:2;
then (x1 "/\" ((x1 => y1) "/\" (x2 => y2))) "\/" (x2 "/\" ((x1 => y1) "/\" (x2 => y2))) [= y1 "\/" y2 by A6, FILTER_0:4;
then (x1 "\/" x2) "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 "\/" y2 by LATTICES:def 11;
then A9: (x1 => y1) "/\" (x2 => y2) [= (x1 "\/" x2) => (y1 "\/" y2) by FILTER_0:def 7;
A10: y1 "/\" (y1 => x1) [= x1 by FILTER_0:def 7;
y1 "/\" ((y1 => x1) "/\" (y2 => x2)) = (y1 "/\" (y1 => x1)) "/\" (y2 => x2) by LATTICES:def 7;
then A11: y1 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 by A10, FILTER_0:2;
A12: y2 "/\" ((y1 => x1) "/\" (y2 => x2)) = (y2 "/\" (y1 => x1)) "/\" (y2 => x2) by LATTICES:def 7;
A13: y2 => x2 in FI by A3, FILTER_0:8;
A14: y2 "/\" (y2 => x2) [= x2 by FILTER_0:def 7;
(y1 => x1) "/\" (y2 "/\" (y2 => x2)) = ((y1 => x1) "/\" y2) "/\" (y2 => x2) by LATTICES:def 7;
then y2 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x2 by A12, A14, FILTER_0:2;
then (y1 "/\" ((y1 => x1) "/\" (y2 => x2))) "\/" (y2 "/\" ((y1 => x1) "/\" (y2 => x2))) [= x1 "\/" x2 by A11, FILTER_0:4;
then (y1 "\/" y2) "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 "\/" x2 by LATTICES:def 11;
then A15: (y1 => x1) "/\" (y2 => x2) [= (y1 "\/" y2) => (x1 "\/" x2) by FILTER_0:def 7;
A16: x1 <=> y1 in FI by A1, FILTER_0:def 11;
then y1 => x1 in FI by FILTER_0:8;
then (y1 => x1) "/\" (y2 => x2) in FI by A13, FILTER_0:8;
then A17: (y1 "\/" y2) => (x1 "\/" x2) in FI by A15, FILTER_0:9;
x1 => y1 in FI by A16, FILTER_0:8;
then (x1 => y1) "/\" (x2 => y2) in FI by A4, FILTER_0:8;
then (x1 "\/" x2) => (y1 "\/" y2) in FI by A9, FILTER_0:9;
then (x1 "\/" x2) <=> (y1 "\/" y2) in FI by A17, FILTER_0:8;
hence [( the L_join of I . (x1,x2)),( the L_join of I . (y1,y2))] in equivalence_wrt FI by FILTER_0:def 11; :: thesis: verum