let L be complete Scott TopLattice; :: thesis:
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:
set IPt = InclPoset the topology of L;
set IPs = InclPoset (sigma L);
A2: sigma L = the topology of L by Th23;
A3: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A4: InclPoset (sigma L) = InclPoset the topology of L by Th23;
thus InclPoset (sigma L) is algebraic :: thesis:

thus for X being Element of (InclPoset (sigma L)) holds
( not compactbelow X is empty & compactbelow X is directed ) by A2; :: according to WAYBEL_8:def 4 :: thesis:
thus InclPoset (sigma L) is up-complete by A4; :: thesis:
let X be Element of (InclPoset (sigma L)); :: according to WAYBEL_8:def 3 :: thesis:
set cX = compactbelow X;
A5: sup (compactbelow X) = union (compactbelow X) by A2, YELLOW_1:22;
set GB = { G where G is Subset of L : ( G in B & G c= X ) } ;
X in sigma L by A3;
then reconsider X' = X as Subset of L ;
X' is open by A3, Th24;
then A6: X = union { G where G is Subset of L : ( G in B & G c= X ) } by YELLOW_8:18;

let x be set ; :: thesis:

hereby :: thesis:

assume x in X ; :: thesis:
then consider GG being set such that
A7: ( x in GG & GG in { G where G is Subset of L : ( G in B & G c= X ) } ) by A6, TARSKI:def 4;
consider G being Subset of L such that
A8: ( G = GG & G in B & G c= 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;
k is compact by A9, WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
then reconsider G = G as Element of (InclPoset (sigma L)) by A2, A3, A9, PRE_TOPC:def 5;
A10: G <= X by A8, YELLOW_1:3;
for X being Subset of L st X is open holds
X is upper by WAYBEL11:def 4;
then uparrow k is compact by Th22;
then G is compact by A2, A9, WAYBEL_3:36;
then G in compactbelow X by A10;
hence x in union (compactbelow X) by A7, A8, TARSKI:def 4; :: thesis:

end;

assume x in union (compactbelow X) ; :: thesis:
then consider G being set such that
A11: ( x in G & G in compactbelow X ) by TARSKI:def 4;
reconsider G = G as Element of (InclPoset (sigma L)) by A11;
G <= X by A11, WAYBEL_8:4;
then G c= X by YELLOW_1:3;
hence x in X by A11; :: thesis:

end;

hence X = "\/" (compactbelow X),(InclPoset (sigma L)) by A5, TARSKI:2; :: thesis:

end;

let V be Element of (InclPoset (sigma L)); :: thesis:
set GB = { G where G is Subset of L : ( G in B & G c= V ) } ;
{ G where G is Subset of L : ( G in B & G c= V ) } c= the carrier of (InclPoset (sigma L))

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { G where G is Subset of L : ( G in B & G c= V ) } ; :: thesis:
then consider G being Subset of L such that
A12: ( G = x & G in B & G c= V ) ;
G is open by A12, YELLOW_8:19;
hence x in the carrier of (InclPoset (sigma L)) by A3, A12, Th24; :: thesis:

end;

then reconsider GB = { G where G is Subset of L : ( G in B & G c= V ) } as Subset of (InclPoset (sigma L)) ;
take GB ; :: thesis:
V in sigma L by A3;
then reconsider V' = V as Subset of L ;
V' is open by A3, Th24;
then V = union GB by YELLOW_8:18;
hence V = sup GB by A2, YELLOW_1:22; :: thesis:
let x be Element of (InclPoset (sigma L)); :: thesis:
assume x in GB ; :: thesis:
then consider G being Subset of L such that
A13: ( G = x & G in B & G c= V ) ;
consider k being Element of L such that
A14: ( G = uparrow k & k in the carrier of (CompactSublatt L) ) by A1, A13;
thus x is co-prime by A13, A14, Th27; :: thesis: