:: deftheorem Def11 defines equivalence_wrt FILTER_0:def 11 :
for L being Lattice
for F being Filter of L
for b₃ being Relation holds
( b₃ = equivalence_wrt F iff ( field b₃ c= the carrier of L & ( for p, q being Element of L holds
( [p,q] in b₃ iff p <=> q in F ) ) ) );