theorem :: WAYBEL10:22

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