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

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