:: deftheorem defines are_equivalence_wrt FILTER_0:def 12 :
for L being Lattice
for F being Filter of L
for p, q being Element of L holds
( p,q are_equivalence_wrt F iff p <=> q in F );