let L be LATTICE; :: thesis:
thus ( L is algebraic implies ( L is continuous & ( for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ) ) ) :: thesis:

assume A1: L is algebraic ; :: thesis:
then A2: ( ( for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ) & L is up-complete & L is satisfying_axiom_K ) by Def4;

let x be Element of L; :: thesis:
A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1, Def4;
then A4: ex_sup_of compactbelow x,L by A2, WAYBEL_0:75;
A5: compactbelow x c= waybelow x by Th6;
consider s being set such that
A6: s in compactbelow x by A3, XBOOLE_0:def 1;
A7: ex_sup_of waybelow x,L by A2, A5, A6, WAYBEL_0:75;
then sup (compactbelow x) <= sup (waybelow x) by A4, Th6, YELLOW_0:34;
then A8: x <= sup (waybelow x) by A2, Def3;
waybelow x is_<=_than x by WAYBEL_3:9;
then sup (waybelow x) <= x by A7, YELLOW_0:def 9;
hence x = sup (waybelow x) by A8, ORDERS_2:25; :: thesis:

end;

then A9: L is satisfying_axiom_of_approximation by WAYBEL_3:def 5;
for x being Element of L holds
( not waybelow x is empty & waybelow x is directed )

let x be Element of L; :: thesis:
not compactbelow x is empty by A1, Def4;
then consider s being set such that
A10: s in compactbelow x by XBOOLE_0:def 1;
compactbelow x c= waybelow x by Th6;
hence ( not waybelow x is empty & waybelow x is directed ) by A10; :: thesis:

end;

hence L is continuous by A2, A9, WAYBEL_3:def 6; :: thesis:
let x, y be Element of L; :: thesis:
assume A11: x << y ; :: thesis:
reconsider D = compactbelow y as non empty directed Subset of L by A1, Def4;
y = sup D by A2, Def3;
then consider d being Element of L such that
A12: ( d in D & x <= d ) by A11, WAYBEL_3:def 1;
take d ; :: thesis:
d is compact by A12, Th4;
hence d in the carrier of (CompactSublatt L) by Def1; :: thesis:
thus ( x <= d & d <= y ) by A12, Th4; :: thesis:

end;

assume that
A13: L is continuous and
A14: for x, y being Element of L st x << y holds
ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) ; :: thesis:
A15: L is up-complete by A13;
A16: for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )

let x be Element of L; :: thesis:
A17: ( not waybelow x is empty & waybelow x is directed ) by A13;

let Y be finite Subset of (compactbelow x); :: thesis:
compactbelow x c= waybelow x by Th6;
then Y is finite Subset of (waybelow x) by XBOOLE_1:1;
then consider b being Element of L such that
A18: ( b in waybelow x & b is_>=_than Y ) by A17, WAYBEL_0:1;
b << x by A18, WAYBEL_3:7;
then consider c being Element of L such that
A19: ( c in the carrier of (CompactSublatt L) & b <= c & c <= x ) by A14;
take c = c; :: thesis:
c is compact by A19, Def1;
hence c in compactbelow x by A19; :: thesis:
thus c is_>=_than Y by A18, A19, YELLOW_0:4; :: thesis:

end;

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

end;

now

let x be Element of L; :: thesis:
L is satisfying_axiom_of_approximation by A13;
then A20: x = sup (waybelow x) by WAYBEL_3:def 5;
not compactbelow x is empty by A16;
then consider s being set such that
A21: s in compactbelow x by XBOOLE_0:def 1;
compactbelow x c= waybelow x by Th6;
then A22: ex_sup_of waybelow x,L by A15, A21, WAYBEL_0:75;

let z be Element of L; :: thesis:
thus ( z is_>=_than waybelow x implies z is_>=_than compactbelow x ) :: thesis:

assume A23: z is_>=_than waybelow x ; :: thesis:

let d be Element of L; :: thesis:
assume d in compactbelow x ; :: thesis:
then A24: ( d <= x & d is compact ) by Th4;
then d << d by WAYBEL_3:def 2;
then d << x by A24, WAYBEL_3:2;
then d in waybelow x by WAYBEL_3:7;
hence d <= z by A23, LATTICE3:def 9; :: thesis:

end;

hence z is_>=_than compactbelow x by LATTICE3:def 9; :: thesis:

end;

thus ( z is_>=_than compactbelow x implies z is_>=_than waybelow x ) :: thesis:

assume A25: z is_>=_than compactbelow x ; :: thesis:

let d be Element of L; :: thesis:
assume d in waybelow x ; :: thesis:
then d << x by WAYBEL_3:7;
then consider k being Element of L such that
A26: ( k in the carrier of (CompactSublatt L) & d <= k & k <= x ) by A14;
k is compact by A26, Def1;
then k in compactbelow x by A26;
then k <= z by A25, LATTICE3:def 9;
hence d <= z by A26, ORDERS_2:26; :: thesis:

end;

hence z is_>=_than waybelow x by LATTICE3:def 9; :: thesis:

end;

hence x = sup (compactbelow x) by A20, A22, YELLOW_0:47; :: thesis:

end;

then L is satisfying_axiom_K by Def3;
hence L is algebraic by A15, A16, Def4; :: thesis: