for I being I_Lattice
for FI being Filter of I
for i, j, k being Element of I st i in Class ((equivalence_wrt FI),k) & j in Class ((equivalence_wrt FI),k) holds
( i "\/" j in Class ((equivalence_wrt FI),k) & i "/\" j in Class ((equivalence_wrt FI),k) )