for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S