for L being Lattice
for p, q being Element of L
for F being Filter of L st p,q are_equivalence_wrt F holds
q,p are_equivalence_wrt F ;