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

assume A2: sup (compactbelow x) <> x ; :: thesis: contradiction
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 A3: sup (downarrow x) <= x by YELLOW_0:32;
A4: ( ex_sup_of compactbelow x,L & ex_sup_of downarrow x,L ) by YELLOW_0:17;
compactbelow x = (downarrow x) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
then sup (compactbelow x) <= sup (downarrow x) by A4, XBOOLE_1:17, YELLOW_0:34;
then A5: sup (compactbelow x) <= x by A3, ORDERS_2:26;

now

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

end;

then A6: x in (downarrow (sup (compactbelow x))) ` by XBOOLE_0:def 5;
set GB = { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } ;
(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:18;
then consider X being set such that
A7: ( x in X & X in { G where G is Subset of L : ( G in B & G c= (downarrow (sup (compactbelow x))) ` ) } ) by A6, TARSKI:def 4;
consider G being Subset of L such that
A8: ( G = X & G in B & G c= (downarrow (sup (compactbelow x))) ` ) by A7;
consider k being Element of L such that
A9: ( G = uparrow k & k in the carrier of (CompactSublatt L) ) by A1, A8;
A10: k <= x by A7, A8, A9, WAYBEL_0:18;
k is compact by A9, WAYBEL_8:def 1;
then A11: k in compactbelow x by A10;
sup (compactbelow x) is_>=_than compactbelow x by YELLOW_0:32;
then k <= sup (compactbelow x) by A11, 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 A8, A9, XBOOLE_0:def 5;
hence contradiction by WAYBEL_0:17; :: thesis: verum

end;

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