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;
set o = the L_join of I;
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 ( [x1,y1] in equivalence_wrt FI & [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
then ( x1 <=> y1 in FI & x2 <=> y2 in FI & x1 <=> y1 = (x1 => y1) "/\" (y1 => x1) & x2 <=> y2 = (x2 => y2) "/\" (y2 => x2) ) by FILTER_0:def 12;
then A1: ( x1 => y1 in FI & x2 => y2 in FI & y1 => x1 in FI & y2 => x2 in FI ) by FILTER_0:def 1;
( x2 "/\" (x1 => y1) = (x1 => y1) "/\" x2 & (x1 => y1) "/\" (x2 "/\" (x2 => y2)) = ((x1 => y1) "/\" x2) "/\" (x2 => y2) & x1 "/\" ((x1 => y1) "/\" (x2 => y2)) = (x1 "/\" (x1 => y1)) "/\" (x2 => y2) & x2 "/\" ((x1 => y1) "/\" (x2 => y2)) = (x2 "/\" (x1 => y1)) "/\" (x2 => y2) & x1 "/\" (x1 => y1) [= y1 & x2 "/\" (x2 => y2) [= y2 ) by FILTER_0:def 8, LATTICES:def 7;
then ( x1 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 & x2 "/\" ((x1 => y1) "/\" (x2 => y2)) [= y2 ) by FILTER_0:2;
then (x1 "/\" ((x1 => y1) "/\" (x2 => y2))) "\/" (x2 "/\" ((x1 => y1) "/\" (x2 => y2))) [= y1 "\/" y2 by FILTER_0:4;
then (x1 "\/" x2) "/\" ((x1 => y1) "/\" (x2 => y2)) [= y1 "\/" y2 by LATTICES:def 11;
then ( (x1 => y1) "/\" (x2 => y2) [= (x1 "\/" x2) => (y1 "\/" y2) & (x1 => y1) "/\" (x2 => y2) in FI ) by A1, FILTER_0:def 1, FILTER_0:def 8;
then A2: (x1 "\/" x2) => (y1 "\/" y2) in FI by FILTER_0:9;
( y2 "/\" (y1 => x1) = (y1 => x1) "/\" y2 & (y1 => x1) "/\" (y2 "/\" (y2 => x2)) = ((y1 => x1) "/\" y2) "/\" (y2 => x2) & y1 "/\" ((y1 => x1) "/\" (y2 => x2)) = (y1 "/\" (y1 => x1)) "/\" (y2 => x2) & y2 "/\" ((y1 => x1) "/\" (y2 => x2)) = (y2 "/\" (y1 => x1)) "/\" (y2 => x2) & y1 "/\" (y1 => x1) [= x1 & y2 "/\" (y2 => x2) [= x2 ) by FILTER_0:def 8, LATTICES:def 7;
then ( y1 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 & y2 "/\" ((y1 => x1) "/\" (y2 => x2)) [= x2 ) by FILTER_0:2;
then (y1 "/\" ((y1 => x1) "/\" (y2 => x2))) "\/" (y2 "/\" ((y1 => x1) "/\" (y2 => x2))) [= x1 "\/" x2 by FILTER_0:4;
then (y1 "\/" y2) "/\" ((y1 => x1) "/\" (y2 => x2)) [= x1 "\/" x2 by LATTICES:def 11;
then ( (y1 => x1) "/\" (y2 => x2) [= (y1 "\/" y2) => (x1 "\/" x2) & (y1 => x1) "/\" (y2 => x2) in FI ) by A1, FILTER_0:def 1, FILTER_0:def 8;
then ( ((x1 "\/" x2) => (y1 "\/" y2)) "/\" ((y1 "\/" y2) => (x1 "\/" x2)) = (x1 "\/" x2) <=> (y1 "\/" y2) & (y1 "\/" y2) => (x1 "\/" x2) in FI ) by FILTER_0:9;
then ( (x1 "\/" x2) <=> (y1 "\/" y2) in FI & the L_join of I . x1,x2 = x1 "\/" x2 & the L_join of I . y1,y2 = y1 "\/" y2 ) by A2, FILTER_0:def 1;
hence [(the L_join of I . x1,x2),(the L_join of I . y1,y2)] in equivalence_wrt FI by FILTER_0:def 12; :: thesis: verum