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

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

hence
closure_op (Image c) = c
by FUNCT_2:63; :: thesis: verumlet 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)

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;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

then A7:
c . x <= "/\" (((uparrow x) /\ (rng c)),L)
by YELLOW_0:33;
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;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

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