for L being Lattice
for F being Filter of L holds F is ClosedSubset of L ;