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 ((equivalence_wrt FI),j) by Def6;
reconsider jj = H₁(I), mm = H₂(I) as BinOp of equivalence_wrt FI by Th13, Th14;
A2: i /\/ FI = Class ((equivalence_wrt FI),i) by Def6;
A3: I /\/ FI = LattStr(# (Class (equivalence_wrt FI)),(jj /\/ (equivalence_wrt FI)),(mm /\/ (equivalence_wrt FI)) #) by Def5;
(i "\/" j) /\/ FI = Class ((equivalence_wrt FI),(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 ((equivalence_wrt FI),(i "/\" j)) by Def6;
hence (i /\/ FI) "/\" (j /\/ FI) = (i "/\" j) /\/ FI by A2, A1, A3, Th3; :: thesis: verum