let I be I_Lattice; :: thesis: for FI being Filter of I
for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )

let FI be Filter of I; :: thesis: for i, j being Element of I holds
( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )

let i, j be Element of I; :: thesis: ( (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI & (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI )
set R = equivalence_wrt FI;
A1: j /\/ FI = Class ((),j) by Def6;
reconsider jj = H1(I), mm = H2(I) as BinOp of equivalence_wrt FI by ;
A2: i /\/ FI = Class ((),i) by Def6;
A3: I /\/ FI = LattStr(# (Class ()),(jj /\/ ()),(mm /\/ ()) #) by Def5;
(i "\/" j) /\/ FI = Class ((),(i "\/" j)) by Def6;
hence (i /\/ FI) "\/" (j /\/ FI) = (i "\/" j) /\/ FI by A2, A1, A3, Th3; :: thesis: (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI
(i "/\" j) /\/ FI = Class ((),(i "/\" j)) by Def6;
hence (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI by A2, A1, A3, Th3; :: thesis: verum