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:

proof

assume A1: L is algebraic ; :: thesis:
then A2: ( L is up-complete & L is satisfying_axiom_K ) ;

now :: thesis:

let x be Element of L; :: thesis:
A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1;
then A4: ex s being object st s in compactbelow x by XBOOLE_0:def 1;
compactbelow x c= waybelow x by Th6;
then A5: ex_sup_of waybelow x,L by A2, A4, WAYBEL_0:75;
ex_sup_of compactbelow x,L by A2, A3, WAYBEL_0:75;
then sup (compactbelow x) <= sup (waybelow x) by A5, Th6, YELLOW_0:34;
then A6: x <= sup (waybelow x) by A2;
waybelow x is_<=_than x by WAYBEL_3:9;
then sup (waybelow x) <= x by A5, YELLOW_0:def 9;
hence x = sup (waybelow x) by A6, ORDERS_2:2; :: thesis:

end;

then A7: 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 )

proof

let x be Element of L; :: thesis:
compactbelow x c= waybelow x by Th6;
hence ( not waybelow x is empty & waybelow x is directed ) by A1; :: thesis:

end;

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

end;

assume that
A11: L is continuous and
A12: 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:

now :: thesis:

let x be Element of L; :: thesis:

A13: now :: thesis:

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

proof

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

now :: thesis:

let d be Element of L; :: thesis:
assume A15: d in compactbelow x ; :: thesis:
then d is compact by Th4;
then A16: d << d by WAYBEL_3:def 2;
d <= x by A15, Th4;
then d << x by A16, WAYBEL_3:2;
then d in waybelow x by WAYBEL_3:7;
hence d <= z by A14, 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:

proof

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

now :: 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
A18: k in the carrier of (CompactSublatt L) and
A19: d <= k and
A20: k <= x by A12;
k is compact by A18, Def1;
then k in compactbelow x by A20;
then k <= z by A17, LATTICE3:def 9;
hence d <= z by A19, ORDERS_2:3; :: thesis:

end;

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

end;

end;

( x = sup (waybelow x) & ex_sup_of waybelow x,L ) by A11, WAYBEL_0:75, WAYBEL_3:def 5;
hence x = sup (compactbelow x) by A13, YELLOW_0:47; :: thesis:

end;

then A21: L is satisfying_axiom_K ;
for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed )

proof

let x be Element of L; :: thesis:

now :: thesis:

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
A22: b in waybelow x and
A23: b is_>=_than Y by A11, WAYBEL_0:1;
b << x by A22, WAYBEL_3:7;
then consider c being Element of L such that
A24: c in the carrier of (CompactSublatt L) and
A25: b <= c and
A26: c <= x by A12;
take c = c; :: thesis:
c is compact by A24, Def1;
hence c in compactbelow x by A26; :: thesis:
thus c is_>=_than Y by A23, A25, YELLOW_0:4; :: thesis:

end;

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

end;

hence L is algebraic by A11, A21; :: thesis: