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 ;
then A4: (i1 "/\" j1) => j2 in FI by Lm1;
A5: j1 => (i2 "\/" j2) in FI by ;
A6: i1 => i2 in FI by ;
then i1 => (i2 "\/" j2) in FI by Lm1;
then A7: (i1 "\/" j1) => (i2 "\/" j2) in FI by ;
A8: j2 => j1 in FI by ;
then A9: (i2 "/\" j2) => j1 in FI by Lm1;
A10: i2 => i1 in FI by ;
then (i2 "/\" j2) => i1 in FI by Lm1;
then A11: (i2 "/\" j2) => (i1 "/\" j1) in FI by ;
A12: j2 => (i1 "\/" j1) in FI by ;
i2 => (i1 "\/" j1) in FI by ;
then A13: (i2 "\/" j2) => (i1 "\/" j1) in FI by ;
(i1 "/\" j1) => i2 in FI by ;
then (i1 "/\" j1) => (i2 "/\" j2) in FI by ;
hence ( (i1 "\/" j1) <=> (i2 "\/" j2) in FI & (i1 "/\" j1) <=> (i2 "/\" j2) in FI ) by ; :: thesis: verum