let L be complete Scott TopLattice; :: thesis: ( ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } implies L is algebraic )
given B being Basis of L such that A1: B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; :: thesis: L is algebraic
thus for x being Element of L holds
( not compactbelow x is empty & compactbelow x is directed ) ; :: according to WAYBEL_8:def 4 :: thesis: ( L is up-complete & L is satisfying_axiom_K )
thus L is up-complete ; :: thesis: L is satisfying_axiom_K
let x be Element of L; :: according to WAYBEL_8:def 3 :: thesis: x = "\/" ((compactbelow x),L)
set y = sup (compactbelow x);
set cx = compactbelow x;
set dx = downarrow x;
set dy = downarrow (sup (compactbelow x));

now :: thesis: not sup (compactbelow x) <> x

for z being Element of L st z in downarrow x holds
z <= x by WAYBEL_0:17;
then x is_>=_than downarrow x by LATTICE3:def 9;
then A2: sup (downarrow x) <= x by YELLOW_0:32;
set GB = { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } ;
A3: compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
A4: sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
( ex_sup_of compactbelow x,L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
then sup (compactbelow x) <= sup (downarrow x) by A3, XBOOLE_1:17, YELLOW_0:34;
then A5: sup (compactbelow x) <= x by A2, ORDERS_2:3;
assume A6: sup (compactbelow x) <> x ; :: thesis: contradiction

now :: thesis: not x in downarrow (sup (compactbelow x))

assume x in downarrow (sup (compactbelow x)) ; :: thesis: contradiction
then x <= sup (compactbelow x) by WAYBEL_0:17;
hence contradiction by A6, A5, ORDERS_2:2; :: thesis: verum

end;

then A7: x in (downarrow (sup (compactbelow x))) ` by XBOOLE_0:def 5;
(downarrow (sup (compactbelow x))) ` = union { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } by WAYBEL11:12, YELLOW_8:9;
then consider X being set such that
A8: x in X and
A9: X in { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } by A7, TARSKI:def 4;
consider G being Subset of L such that
A10: G = X and
A11: G in B and
A12: G c= (downarrow (sup (compactbelow x))) ` by A9;
consider k being Element of L such that
A13: G = uparrow k and
A14: k in the carrier of (CompactSublatt L) by A1, A11;
A15: k is compact by A14, WAYBEL_8:def 1;
k <= x by A8, A10, A13, WAYBEL_0:18;
then k in compactbelow x by A15;
then k <= sup (compactbelow x) by A4, LATTICE3:def 9;
then sup (compactbelow x) in uparrow k by WAYBEL_0:18;
then ( sup (compactbelow x) <= sup (compactbelow x) & not sup (compactbelow x) in downarrow (sup (compactbelow x)) ) by A12, A13, XBOOLE_0:def 5;
hence contradiction by WAYBEL_0:17; :: thesis: verum

end;

hence x = "\/" ((compactbelow x),L) ; :: thesis: verum