for L being complete LATTICE holds ClOpers L,(ClosureSystems L) opp are_isomorphic