let L be complete Scott TopLattice; :: thesis:
set P = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ;
{ (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } c= bool the carrier of L

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; :: thesis:
then ex k being Element of L st
( x = uparrow k & k in the carrier of (CompactSublatt L) ) ;
hence x in bool the carrier of L ; :: thesis:

end;

then reconsider P = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } as Subset-Family of L ;
reconsider P = P as Subset-Family of L ;
A1: P c= the topology of L

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in P ; :: thesis:
then consider k being Element of L such that
A2: x = uparrow k and
A3: k in the carrier of (CompactSublatt L) ;
k is compact by A3, WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
hence x in the topology of L by A2, PRE_TOPC:def 2; :: thesis:

end;

assume A4: L is algebraic ; :: thesis:

let x be Point of L; :: thesis:
set B = { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } ;
{ (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } c= bool the carrier of L

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } ; :: thesis:
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y in bool the carrier of L ; :: thesis:

end;

then reconsider B = { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
B is Basis of x

let y be Subset of L; :: according to TOPS_2:def 1 :: thesis:
assume y in B ; :: thesis:
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y is open by A1, PRE_TOPC:def 2; :: thesis:

end;

B is x -quasi_basis

suppose B is empty ; :: thesis:

then Intersect B = the carrier of L by SETFAM_1:def 9;
hence x in Intersect B ; :: thesis:

end;

suppose A6: not B is empty ; :: thesis:

A7: now :: thesis:

let Y be set ; :: thesis:
assume Y in B ; :: thesis:
then ex k being Element of L st
( Y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence x in Y ; :: thesis:

end;

Intersect B = meet B by A6, SETFAM_1:def 9;
hence x in Intersect B by A6, A7, SETFAM_1:def 1; :: thesis:

end;

end;

end;

hence x in Intersect B ; :: according to YELLOW_8:def 1 :: thesis:
reconsider x9 = x as Element of L ;
let S be Subset of L; :: thesis:
assume that
A8: S is open and
A9: x in S ; :: thesis:
A10: x = sup (compactbelow x9) by A4, WAYBEL_8:def 3;
S is inaccessible by A8, WAYBEL11:def 4;
then compactbelow x9 meets S by A9, A10, WAYBEL11:def 1;
then consider k being object such that
A11: k in compactbelow x9 and
A12: k in S by XBOOLE_0:3;
reconsider k = k as Element of L by A11;
A13: compactbelow x9 = (downarrow x9) /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
then k in downarrow x9 by A11, XBOOLE_0:def 4;
then k <= x9 by WAYBEL_0:17;
then A14: x in uparrow k by WAYBEL_0:18;
take V = uparrow k; :: thesis:
k in the carrier of (CompactSublatt L) by A11, A13, XBOOLE_0:def 4;
then uparrow k in P ;
hence V in B by A14; :: thesis:
S is upper by A8, WAYBEL11:def 4;
hence V c= S by A12, WAYBEL11:42; :: thesis:

end;

hence B is Basis of x by A5; :: thesis:

end;

then reconsider B = B as Basis of x ;
take B = B; :: thesis:
thus B c= P :: thesis:

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in B ; :: thesis:
then ex k being Element of L st
( y = uparrow k & uparrow k in P & x in uparrow k ) ;
hence y in P ; :: thesis:

end;

end;

then P is Basis of L by A1, YELLOW_8:14;
hence ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } ; :: thesis: