theorem Th21: :: WAYBEL10:21
for L being complete LATTICE
for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S