for L being Lattice
for F being Filter of L holds equivalence_wrt F is Relation of the carrier of L