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

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