theorem :: FILTER_0:69

for L being Lattice
for p, q being Element of L
for F being Filter of L holds
( p,q are_equivalence_wrt F iff [p,q] in equivalence_wrt F ) by Def11;