let L be complete LATTICE; :: thesis: for S being strict closure System of L holds ((ClImageMap L) ") . S = closure_op S
let S be strict full infs-inheriting SubRelStr of L; :: thesis: ((ClImageMap L) ") . S = closure_op S
A1: closure_op S is Element of (ClOpers L) by Th10;
(ClImageMap L) . (closure_op S) = Image (closure_op S) by Def4
.= S by Th18 ;
hence ((ClImageMap L) ") . S = closure_op S by A1, FUNCT_2:26; :: thesis: verum