for L being complete LATTICE holds (ClImageMap L) " is Function of ((ClosureSystems L) opp),(ClOpers L)