let L be lower-bounded algebraic LATTICE; :: thesis: for c being closure Function of L,L st c is directed-sups-preserving holds
Image c is algebraic LATTICE
let c be closure Function of L,L; :: thesis: ( c is directed-sups-preserving implies Image c is algebraic LATTICE )
assume A1: c is directed-sups-preserving ; :: thesis: Image c is algebraic LATTICE
c is idempotent by WAYBEL_1:def 13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:37;

A2: now

let x be Element of Imc; :: thesis: ( not compactbelow x is empty & compactbelow x is directed )

now

let y, z be Element of Imc; :: thesis: ( y in compactbelow x & z in compactbelow x implies ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v ) )
assume that
A3: y in compactbelow x and
A4: z in compactbelow x ; :: thesis: ex v being Element of the carrier of Imc st
( v in compactbelow x & y <= v & z <= v )
A5: ( y <= x & y is compact ) by A3, Th4;
A6: ( z <= x & z is compact ) by A4, Th4;
then A7: ( y << y & z << z ) by A5, WAYBEL_3:def 2;
take v = y "\/" z; :: thesis: ( v in compactbelow x & y <= v & z <= v )
A8: v <= x by A5, A6, YELLOW_0:22;
( y <= v & z <= v ) by YELLOW_0:22;
then ( y << v & z << v ) by A7, WAYBEL_3:2;
then v << v by WAYBEL_3:3;
then v is compact by WAYBEL_3:def 2;
hence ( v in compactbelow x & y <= v & z <= v ) by A8, YELLOW_0:22; :: thesis: verum

end;

hence ( not compactbelow x is empty & compactbelow x is directed ) by WAYBEL_0:def 1; :: thesis: verum

end;

now

let x be Element of Imc; :: thesis: x = sup (compactbelow x)
consider y being Element of L such that
A9: c . y = x by YELLOW_2:12;
A10: ( not compactbelow y is empty & compactbelow y is directed ) by Def4;
then A11: c preserves_sup_of compactbelow y by A1, WAYBEL_0:def 37;
A12: ex_sup_of compactbelow y,L by A10, WAYBEL_0:75;
compactbelow y = (downarrow y) /\ the carrier of (CompactSublatt L) by Th5;
then compactbelow y = (downarrow y) /\ ([#] (CompactSublatt L)) ;
then A13: c .: (compactbelow y) c= (c .: (downarrow y)) /\ (c .: ([#] (CompactSublatt L))) by RELAT_1:154;
A14: c is monotone by A1, YELLOW_2:18;
compactbelow x is directed by A2;
then A15: ex_sup_of compactbelow x,Imc by WAYBEL_0:75;
A16: ex_sup_of c .: (compactbelow y),Imc by YELLOW_0:17;
c .: (compactbelow y) c= rng c by RELAT_1:144;
then A17: c .: (compactbelow y) is Subset of Imc by YELLOW_0:def 15;
A18: ex_sup_of c .: (compactbelow y),L by YELLOW_0:17;
A19: c . (sup (compactbelow y)) = sup (c .: (compactbelow y)) by A11, A12, WAYBEL_0:def 31;
sup (compactbelow y) in the carrier of L ;
then sup (compactbelow y) in dom c by FUNCT_2:def 1;
then sup (c .: (compactbelow y)) in rng c by A19, FUNCT_1:def 5;
then sup (c .: (compactbelow y)) in the carrier of (Image c) by YELLOW_0:def 15;
then A20: sup (c .: (compactbelow y)) = "\/" (c .: (compactbelow y)),Imc by A17, A18, YELLOW_0:65;
A21: c . y = c . (sup (compactbelow y)) by Def3
.= sup (c .: (compactbelow y)) by A11, A12, WAYBEL_0:def 31 ;
A22: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th25;

now

let z be set ; :: thesis: ( z in c .: (compactbelow y) implies z in compactbelow x )
assume A23: z in c .: (compactbelow y) ; :: thesis: z in compactbelow x
then consider v being set such that
A24: ( v in dom c & v in compactbelow y & z = c . v ) by FUNCT_1:def 12;
reconsider v = v as Element of L by A24;
z in rng c by A24, FUNCT_1:def 5;
then reconsider z1 = z as Element of Imc by YELLOW_0:def 15;
z in c .: ([#] (CompactSublatt L)) by A13, A23, XBOOLE_0:def 4;
then z in [#] (CompactSublatt (Image c)) by A22;
then A25: z1 is compact by Def1;
v <= y by A24, Th4;
then c . v <= c . y by A14, WAYBEL_1:def 2;
then z1 <= x by A9, A24, YELLOW_0:61;
hence z in compactbelow x by A25; :: thesis: verum

end;

then c .: (compactbelow y) c= compactbelow x by TARSKI:def 3;
then A26: x <= sup (compactbelow x) by A9, A15, A16, A20, A21, YELLOW_0:34;
for b being Element of Imc st b in compactbelow x holds
b <= x by Th4;
then x is_>=_than compactbelow x by LATTICE3:def 9;
then sup (compactbelow x) <= x by YELLOW_0:32;
hence x = sup (compactbelow x) by A26, ORDERS_2:25; :: thesis: verum

end;

then Imc is satisfying_axiom_K by Def3;
hence Image c is algebraic LATTICE by A2, Def4; :: thesis: verum