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