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

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