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