let L be LATTICE; :: thesis: ( L is algebraic iff ( 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 ) ) ) )
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: ( 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 ) ) implies L is algebraic )

proof

assume A1: L is algebraic ; :: thesis: ( 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 ) ) )
then A2: ( L is up-complete & L is satisfying_axiom_K ) by Def4;

now

let x be Element of L; :: thesis: x = sup (waybelow x)
A3: ( not compactbelow x is empty & compactbelow x is directed ) by A1, Def4;
then A4: ex s being set 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, Def3;
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: verum

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: ( not waybelow x is empty & waybelow x is directed )
compactbelow x c= waybelow x by Th6;
hence ( not waybelow x is empty & waybelow x is directed ) by A1, Def4; :: thesis: verum

end;

hence L is continuous by A2, A7, WAYBEL_3:def 6; :: thesis: 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 )
let x, y be Element of L; :: thesis: ( x << y implies ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y ) )
reconsider D = compactbelow y as non empty directed Subset of L by A1, Def4;
assume A8: x << y ; :: thesis: ex k being Element of L st
( k in the carrier of (CompactSublatt L) & x <= k & k <= y )
y = sup D by A2, Def3;
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 in the carrier of (CompactSublatt L) & x <= d & d <= y )
d is compact by A9, Th4;
hence d in the carrier of (CompactSublatt L) by Def1; :: thesis: ( x <= d & d <= y )
thus ( x <= d & d <= y ) by A9, A10, Th4; :: thesis: verum

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: L is algebraic

now

let x be Element of L; :: thesis: x = sup (compactbelow x)

A13: now

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

proof

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

now

let d be Element of L; :: thesis: ( d in compactbelow x implies d <= z )
assume A15: d in compactbelow x ; :: thesis: d <= z
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: verum

end;

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

end;

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

proof

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

now

let d be Element of L; :: thesis: ( d in waybelow x implies d <= z )
assume d in waybelow x ; :: thesis: d <= z
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: verum

end;

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

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: verum

end;

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

proof

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

now

let Y be finite Subset of (compactbelow x); :: thesis: ex c being Element of L st
( c in compactbelow x & c is_>=_than Y )
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 in compactbelow x & c is_>=_than Y )
c is compact by A24, Def1;
hence c in compactbelow x by A26; :: thesis: c is_>=_than Y
thus c is_>=_than Y by A23, A25, YELLOW_0:4; :: thesis: verum

end;

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

end;

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