let I be I_Lattice; :: thesis: for FI being Filter of I
for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
let FI be Filter of I; :: thesis: for i, j being Element of I holds
( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
let i, j be Element of I; :: thesis: ( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI )
( i in Class ((equivalence_wrt FI),j) iff [i,j] in equivalence_wrt FI ) by EQREL_1:19;
hence ( i in Class ((equivalence_wrt FI),j) iff i <=> j in FI ) by FILTER_0:def 11; :: thesis: verum