let L be lower-bounded algebraic LATTICE; :: thesis:
let c be closure Function of L,L; :: thesis:
assume A1: c is directed-sups-preserving ; :: thesis:
c is idempotent by WAYBEL_1:def 13;
then reconsider Imc = Image c as complete LATTICE by A1, YELLOW_2:35;

A2: now :: thesis:

let x be Element of Imc; :: thesis:

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

end;

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

end;

let x be Element of Imc; :: thesis:
consider y being Element of L such that
A9: c . y = x by YELLOW_2:10;
sup (compactbelow y) in the carrier of L ;
then A10: sup (compactbelow y) in dom c by FUNCT_2:def 1;
( not compactbelow y is empty & compactbelow y is directed ) by Def4;
then A11: ( c preserves_sup_of compactbelow y & ex_sup_of compactbelow y,L ) by A1, WAYBEL_0:75, WAYBEL_0:def 37;
then c . (sup (compactbelow y)) = sup (c .: (compactbelow y)) by WAYBEL_0:def 31;
then sup (c .: (compactbelow y)) in rng c by A10, FUNCT_1:def 3;
then A12: ( ex_sup_of c .: (compactbelow y),L & sup (c .: (compactbelow y)) in the carrier of (Image c) ) by YELLOW_0:17, YELLOW_0:def 15;
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 A13: sup (compactbelow x) <= x by YELLOW_0:32;
A14: c .: ([#] (CompactSublatt L)) c= [#] (CompactSublatt (Image c)) by A1, Th23;
A15: c is monotone by A1, YELLOW_2:16;
compactbelow y = (downarrow y) /\ ([#] (CompactSublatt L)) by Th5;
then A16: c .: (compactbelow y) c= (c .: (downarrow y)) /\ (c .: ([#] (CompactSublatt L))) by RELAT_1:121;

let z be object ; :: thesis:
assume A17: z in c .: (compactbelow y) ; :: thesis:
then consider v being object such that
A18: v in dom c and
A19: v in compactbelow y and
A20: z = c . v by FUNCT_1:def 6;
z in rng c by A18, A20, FUNCT_1:def 3;
then reconsider z1 = z as Element of Imc by YELLOW_0:def 15;
reconsider v = v as Element of L by A18;
v <= y by A19, Th4;
then c . v <= c . y by A15, WAYBEL_1:def 2;
then A21: z1 <= x by A9, A20, YELLOW_0:60;
z in c .: ([#] (CompactSublatt L)) by A16, A17, XBOOLE_0:def 4;
then z1 is compact by A14, Def1;
hence z in compactbelow x by A21; :: thesis:

end;

then A22: c .: (compactbelow y) c= compactbelow x ;
compactbelow x is directed by A2;
then A23: ex_sup_of compactbelow x,Imc by WAYBEL_0:75;
c .: (compactbelow y) c= rng c by RELAT_1:111;
then c .: (compactbelow y) is Subset of Imc by YELLOW_0:def 15;
then A24: ( ex_sup_of c .: (compactbelow y),Imc & sup (c .: (compactbelow y)) = "\/" ((c .: (compactbelow y)),Imc) ) by A12, YELLOW_0:64;
c . y = c . (sup (compactbelow y)) by Def3
.= sup (c .: (compactbelow y)) by A11, WAYBEL_0:def 31 ;
then x <= sup (compactbelow x) by A9, A23, A24, A22, YELLOW_0:34;
hence x = sup (compactbelow x) by A13, ORDERS_2:2; :: thesis:

end;

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