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

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