let L be complete LATTICE; :: thesis: for c being closure Function of L,L holds closure_op (Image c) = c
let c be closure Function of L,L; :: thesis: closure_op (Image c) = c

now

let x be Element of L; :: thesis: (closure_op (Image c)) . x = c . x
( x = (id L) . x & id L <= c ) by TMAP_1:91, WAYBEL_1:def 14;
then ( dom c = the carrier of L & x <= c . x ) by FUNCT_2:def 1, YELLOW_2:10;
then ( c . x in uparrow x & c . x in rng c ) by FUNCT_1:def 5, WAYBEL_0:18;
then c . x in (uparrow x) /\ (rng c) by XBOOLE_0:def 4;
then A1: c . x >= "/\" ((uparrow x) /\ (rng c)),L by YELLOW_2:24;
c . x is_<=_than (uparrow x) /\ (rng c)

proof

let z be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not z in (uparrow x) /\ (rng c) or c . x <= z )
assume z in (uparrow x) /\ (rng c) ; :: thesis: c . x <= z
then A2: ( z in uparrow x & z in rng c ) by XBOOLE_0:def 4;
then consider a being set such that
A3: ( a in dom c & z = c . a ) by FUNCT_1:def 5;
reconsider a = a as Element of L by A3;
( x <= c . a & c is monotone ) by A2, A3, WAYBEL_0:18;
then ( c . x <= c . (c . a) & c is idempotent ) by WAYBEL_1:def 2;
hence c . x <= z by A3, YELLOW_2:20; :: thesis: verum

end;

then A4: c . x <= "/\" ((uparrow x) /\ (rng c)),L by YELLOW_0:33;
rng c = the carrier of (Image c) by YELLOW_0:def 15;
hence (closure_op (Image c)) . x = "/\" ((uparrow x) /\ (rng c)),L by Def6
.= c . x by A1, A4, ORDERS_2:25 ;
:: thesis: verum

end;

hence closure_op (Image c) = c by FUNCT_2:113; :: thesis: verum