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) } )
assume Z: 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) }
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 set ; :: 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 ;
A2: P c= the topology of L

proof

let x be set ; :: 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
A3: ( x = uparrow k & 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 A3, PRE_TOPC:def 5; :: thesis: verum

end;

now

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 set ; :: 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

thus B c= the topology of L :: according to YELLOW_8:def 2 :: thesis: ( x in Intersect B & ( 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₁ ) ) ) )

proof

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

end;

now

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 10;
hence x in Intersect B ; :: thesis: verum

end;

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

then A5: Intersect B = meet B by SETFAM_1:def 10;

now

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;

hence x in Intersect B by A4, A5, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

hence x in Intersect B ; :: 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₁ ) )
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
A6: S is open and
A7: x in S ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in B & b₁ c= S )
reconsider x' = x as Element of L ;
A8: x = sup (compactbelow x') by Z, WAYBEL_8:def 3;
S is inaccessible_by_directed_joins by A6, WAYBEL11:def 4;
then compactbelow x' meets S by A7, A8, WAYBEL11:def 1;
then consider k being set such that
A9: ( k in compactbelow x' & k in S ) by XBOOLE_0:3;
A10: compactbelow x' = (downarrow x') /\ the carrier of (CompactSublatt L) by WAYBEL_8:5;
reconsider k = k as Element of L by A9;
take V = uparrow k; :: thesis: ( V in B & V c= S )
k in the carrier of (CompactSublatt L) by A9, A10, XBOOLE_0:def 4;
then A11: uparrow k in P ;
k in downarrow x' by A9, A10, XBOOLE_0:def 4;
then k <= x' by WAYBEL_0:17;
then x in uparrow k by WAYBEL_0:18;
hence V in B by A11; :: thesis: V c= S
S is upper by A6, WAYBEL11:def 4;
hence V c= S by A9, WAYBEL11:42; :: 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 set ; :: 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 A2, YELLOW_8:23;
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