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 :: thesis: for x being Element of L holds (closure_op (Image c)) . x = c . x

let x be Element of L; :: thesis: (closure_op (Image c)) . x = c . x
A1: id L <= c by WAYBEL_1:def 14;
x = (id L) . x ;
then x <= c . x by A1, YELLOW_2:9;
then A2: c . x in uparrow x by WAYBEL_0:18;
dom c = the carrier of L by FUNCT_2:def 1;
then c . x in rng c by FUNCT_1:def 3;
then c . x in (uparrow x) /\ (rng c) by A2, XBOOLE_0:def 4;
then A3: c . x >= "/\" (((uparrow x) /\ (rng c)),L) by YELLOW_2:22;
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 A4: z in (uparrow x) /\ (rng c) ; :: thesis: c . x <= z
then z in rng c by XBOOLE_0:def 4;
then consider a being object such that
A5: a in dom c and
A6: z = c . a by FUNCT_1:def 3;
reconsider a = a as Element of L by A5;
z in uparrow x by A4, XBOOLE_0:def 4;
then x <= c . a by A6, WAYBEL_0:18;
then c . x <= c . (c . a) by WAYBEL_1:def 2;
hence c . x <= z by A6, YELLOW_2:18; :: thesis: verum

end;

then A7: 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 Def5
.= c . x by A3, A7, ORDERS_2:2 ;
:: thesis: verum

end;

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