let I be I_Lattice; :: thesis: for FI being Filter of I

for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

let FI be Filter of I; :: thesis: for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

let i1, i2, j1, j2 be Element of I; :: thesis: ( i1 <=> i2 in FI & j1 <=> j2 in FI implies ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) )

assume that

A1: i1 <=> i2 in FI and

A2: j1 <=> j2 in FI ; :: thesis: ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

A3: j1 => j2 in FI by A2, FILTER_0:8;

then A4: (i1 "/\" j1) => j2 in FI by Lm1;

A5: j1 => (i2 "\/" j2) in FI by A3, Lm1;

A6: i1 => i2 in FI by A1, FILTER_0:8;

then i1 => (i2 "\/" j2) in FI by Lm1;

then A7: (i1 "\/" j1) => (i2 "\/" j2) in FI by A5, Lm2;

A8: j2 => j1 in FI by A2, FILTER_0:8;

then A9: (i2 "/\" j2) => j1 in FI by Lm1;

A10: i2 => i1 in FI by A1, FILTER_0:8;

then (i2 "/\" j2) => i1 in FI by Lm1;

then A11: (i2 "/\" j2) => (i1 "/\" j1) in FI by A9, Lm3;

A12: j2 => (i1 "\/" j1) in FI by A8, Lm1;

i2 => (i1 "\/" j1) in FI by A10, Lm1;

then A13: (i2 "\/" j2) => (i1 "\/" j1) in FI by A12, Lm2;

(i1 "/\" j1) => i2 in FI by A6, Lm1;

then (i1 "/\" j1) => (i2 "/\" j2) in FI by A4, Lm3;

hence ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) by A11, A7, A13, FILTER_0:8; :: thesis: verum

for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

let FI be Filter of I; :: thesis: for i1, i2, j1, j2 being Element of I st i1 <=> i2 in FI & j1 <=> j2 in FI holds

( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

let i1, i2, j1, j2 be Element of I; :: thesis: ( i1 <=> i2 in FI & j1 <=> j2 in FI implies ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) )

assume that

A1: i1 <=> i2 in FI and

A2: j1 <=> j2 in FI ; :: thesis: ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI )

A3: j1 => j2 in FI by A2, FILTER_0:8;

then A4: (i1 "/\" j1) => j2 in FI by Lm1;

A5: j1 => (i2 "\/" j2) in FI by A3, Lm1;

A6: i1 => i2 in FI by A1, FILTER_0:8;

then i1 => (i2 "\/" j2) in FI by Lm1;

then A7: (i1 "\/" j1) => (i2 "\/" j2) in FI by A5, Lm2;

A8: j2 => j1 in FI by A2, FILTER_0:8;

then A9: (i2 "/\" j2) => j1 in FI by Lm1;

A10: i2 => i1 in FI by A1, FILTER_0:8;

then (i2 "/\" j2) => i1 in FI by Lm1;

then A11: (i2 "/\" j2) => (i1 "/\" j1) in FI by A9, Lm3;

A12: j2 => (i1 "\/" j1) in FI by A8, Lm1;

i2 => (i1 "\/" j1) in FI by A10, Lm1;

then A13: (i2 "\/" j2) => (i1 "\/" j1) in FI by A12, Lm2;

(i1 "/\" j1) => i2 in FI by A6, Lm1;

then (i1 "/\" j1) => (i2 "/\" j2) in FI by A4, Lm3;

hence ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) by A11, A7, A13, FILTER_0:8; :: thesis: verum