let L be complete Scott TopLattice; :: thesis: ( L is algebraic implies ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } )
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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } or x in bool the carrier of L )
assume x in { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; :: thesis: x in bool the carrier of L
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: verum

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in P or x in the topology of L )
assume x in P ; :: thesis: x in the topology of L
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: verum

end;

assume A4: L is algebraic ; :: thesis: ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }

now :: thesis: for x being Point of L ex B being Basis of x st B c= P

let x be Point of L; :: thesis: ex B being Basis of x st B c= P
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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } or y in bool the carrier of L )
assume y in { (uparrow k) where k is Element of L : ( uparrow k in P & x in uparrow k ) } ; :: thesis: y in bool the carrier of L
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: verum

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

proof

A5: B is open

proof

let y be Subset of L; :: according to TOPS_2:def 1 :: thesis: ( not y in B or y is open )
assume y in B ; :: thesis: y is open
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: verum

end;

B is x -quasi_basis

proof

now :: thesis: x in Intersect B

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: x in Intersect B

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

end;

suppose A6: not B is empty ; :: thesis: x in Intersect B

A7: now :: thesis: for Y being set st Y in B holds
x in Y

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

end;

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

end;

end;

end;

hence x in Intersect B ; :: according to YELLOW_8:def 1 :: thesis: for b₁ being Element of bool the carrier of L holds
( not b₁ is open or not x in b₁ or ex b₂ being Element of bool the carrier of L st
( b₂ in B & b₂ c= b₁ ) )
reconsider x9 = x as Element of L ;
let S be Subset of L; :: thesis: ( not S is open or not x in S or ex b₁ being Element of bool the carrier of L st
( b₁ in B & b₁ c= S ) )
assume that
A8: S is open and
A9: x in S ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in B & b₁ c= S )
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: ( V in B & V c= S )
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: V c= S
S is upper by A8, WAYBEL11:def 4;
hence V c= S by A12, WAYBEL11:42; :: thesis: verum

end;

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

end;

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

proof

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

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