let L be complete Scott TopLattice; :: thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of (InclPoset (sigma L)) ex VV being Subset of (InclPoset (sigma L)) st
( V = sup VV & ( for W being Element of (InclPoset (sigma L)) st W in VV holds
W is co-prime ) ) ) 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 IPt = InclPoset the topology of L;
set IPs = InclPoset (sigma L);
A1: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
set B = { (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 B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } as Subset-Family of L ;
assume that
A2: InclPoset (sigma L) is algebraic and
A3: for V being Element of (InclPoset (sigma L)) ex X being Subset of (InclPoset (sigma L)) st
( V = sup X & ( for x being Element of (InclPoset (sigma L)) st x in X holds
x is co-prime ) ) ; :: thesis: ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
InclPoset (sigma L) = InclPoset the topology of L by Th23;
then reconsider ips = InclPoset (sigma L) as algebraic LATTICE by A2;
reconsider B = B as Subset-Family of L ;
A4: B c= the topology of L

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in the topology of L )
assume x in B ; :: thesis: x in the topology of L
then consider k being Element of L such that
A5: x = uparrow k and
A6: k in the carrier of (CompactSublatt L) ;
k is compact by A6, 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 A5, PRE_TOPC:def 5; :: thesis: verum

end;

A7: sigma L = the topology of L by Th23;
( ips is continuous & ( for x being Element of L ex X being Basis of x st
for Y being Subset of L st Y in X holds
( Y is open & Y is filtered ) ) ) by A3, Th39;
then for x being Element of L holds x = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by Th37;
then A8: L is continuous by Th38;

now

let x be Point of L; :: thesis: ex Bx being Basis of x st Bx c= B
set Bx = { (uparrow k) where k is Element of L : ( uparrow k in B & x in uparrow k ) } ;
{ (uparrow k) where k is Element of L : ( uparrow k in B & 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 B & 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 B & 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 B & x in uparrow k ) ;
hence y in bool the carrier of L ; :: thesis: verum

end;

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

proof

A90: Bx is open

proof

let y be Subset of L; :: according to TOPS_2:def 1 :: thesis: ( not y in Bx or y is open )
assume y in Bx ; :: thesis: y is open
then ex k being Element of L st
( y = uparrow k & uparrow k in B & x in uparrow k ) ;
hence y is open by A4, PRE_TOPC:def 5; :: thesis: verum

end;

Bx is x -quasi_basis

proof

now

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

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

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

end;

suppose A9: not Bx is empty ; :: thesis: x in Intersect Bx

A10: now

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

end;

Intersect Bx = meet Bx by A9, SETFAM_1:def 10;
hence x in Intersect Bx by A9, A10, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

hence x in Intersect Bx ; :: according to YELLOW_8:def 2 :: 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 Bx & 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 Bx & b₁ c= S ) )
assume that
A11: S is open and
A12: x in S ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in Bx & b₁ c= S )
reconsider S9 = S as Element of (InclPoset the topology of L) by A7, A1, A11, PRE_TOPC:def 5;
S9 = sup (compactbelow S9) by A2, A7, WAYBEL_8:def 3;
then S9 = union (compactbelow S9) by YELLOW_1:22;
then consider UA being set such that
A13: x in UA and
A14: UA in compactbelow S9 by A12, TARSKI:def 4;
reconsider UA = UA as Element of (InclPoset the topology of L) by A14;
UA is compact by A14, WAYBEL_8:4;
then A15: UA << UA by WAYBEL_3:def 2;
UA in the topology of L by A7, A1;
then reconsider UA9 = UA as Subset of L ;
UA <= S9 by A14, WAYBEL_8:4;
then A16: UA c= S by YELLOW_1:3;
consider F being Subset of (InclPoset (sigma L)) such that
A17: UA = sup F and
A18: for x being Element of (InclPoset (sigma L)) st x in F holds
x is co-prime by A3, A7;
reconsider F9 = F as Subset-Family of L by A1, XBOOLE_1:1;
A19: UA = union F by A7, A17, YELLOW_1:22;
F9 is open

proof

let P be Subset of L; :: according to TOPS_2:def 1 :: thesis: ( not P in F9 or P is open )
assume P in F9 ; :: thesis: P is open
hence P is open by A7, A1, PRE_TOPC:def 5; :: thesis: verum

end;

then consider G being finite Subset of F9 such that
A20: UA c= union G by A19, A15, WAYBEL_3:34;
union G c= union F by ZFMISC_1:95;
then A21: UA = union G by A19, A20, XBOOLE_0:def 10;
reconsider G = G as finite Subset-Family of L by XBOOLE_1:1;
consider Gg being finite Subset-Family of L such that
A22: Gg c= G and
A23: union Gg = union G and
A24: for g being Subset of L st g in Gg holds
not g c= union (Gg \ {g}) by Th1;
consider U1 being set such that
A25: x in U1 and
A26: U1 in Gg by A13, A20, A23, TARSKI:def 4;
A27: Gg c= F by A22, XBOOLE_1:1;
then U1 in F by A26;
then reconsider U1 = U1 as Element of (InclPoset (sigma L)) ;
U1 in the topology of L by A7, A1;
then reconsider U19 = U1 as Subset of L ;
set k = inf U19;
A28: U19 c= uparrow (inf U19)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in U19 or x in uparrow (inf U19) )
assume A29: x in U19 ; :: thesis: x in uparrow (inf U19)
then reconsider x9 = x as Element of L ;
inf U19 is_<=_than U19 by YELLOW_0:33;
then inf U19 <= x9 by A29, LATTICE3:def 8;
hence x in uparrow (inf U19) by WAYBEL_0:18; :: thesis: verum

end;

U1 is co-prime by A18, A26, A27;
then A30: ( U19 is filtered & U19 is upper ) by Th27;

now

set D = { ((downarrow u) `) where u is Element of L : u in U19 } ;
A31: { ((downarrow u) `) where u is Element of L : u in U19 } c= the topology of L

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in { ((downarrow u) `) where u is Element of L : u in U19 } or d in the topology of L )
assume d in { ((downarrow u) `) where u is Element of L : u in U19 } ; :: thesis: d in the topology of L
then consider u being Element of L such that
A32: d = (downarrow u) ` and
u in U19 ;
(downarrow u) ` is open by WAYBEL11:12;
hence d in the topology of L by A32, PRE_TOPC:def 5; :: thesis: verum

end;

consider u being set such that
A33: u in U19 by A25;
reconsider u = u as Element of L by A33;
(downarrow u) ` in { ((downarrow u) `) where u is Element of L : u in U19 } by A33;
then reconsider D = { ((downarrow u) `) where u is Element of L : u in U19 } as non empty Subset of (InclPoset the topology of L) by A31, YELLOW_1:1;
assume A34: not inf U19 in U19 ; :: thesis: contradiction

now

assume not UA c= union D ; :: thesis: contradiction
then consider l being set such that
A35: l in UA9 and
A36: not l in union D by TARSKI:def 3;
reconsider l = l as Element of L by A35;
consider Uk being set such that
A37: l in Uk and
A38: Uk in Gg by A20, A23, A35, TARSKI:def 4;
A39: Gg c= F by A22, XBOOLE_1:1;
then Uk in F by A38;
then reconsider Uk = Uk as Element of (InclPoset (sigma L)) ;
Uk in the topology of L by A7, A1;
then reconsider Uk9 = Uk as Subset of L ;
Uk is co-prime by A18, A38, A39;
then A40: ( Uk9 is filtered & Uk9 is upper ) by Th27;

now

assume not l is_<=_than U19 ; :: thesis: contradiction
then consider m being Element of L such that
A41: m in U19 and
A42: not l <= m by LATTICE3:def 8;
(downarrow m) ` in D by A41;
then not l in (downarrow m) ` by A36, TARSKI:def 4;
then l in downarrow m by XBOOLE_0:def 5;
hence contradiction by A42, WAYBEL_0:17; :: thesis: verum

end;

then l <= inf U19 by YELLOW_0:33;
then A43: inf U19 in Uk9 by A37, A40, WAYBEL_0:def 20;
A44: inf U19 is_<=_than U19 by YELLOW_0:33;
A45: U19 c= Uk

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in U19 or u in Uk )
assume A46: u in U19 ; :: thesis: u in Uk
then reconsider d = u as Element of L ;
inf U19 <= d by A44, A46, LATTICE3:def 8;
hence u in Uk by A40, A43, WAYBEL_0:def 20; :: thesis: verum

end;

U19 c= union (Gg \ {U19})

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in U19 or u in union (Gg \ {U19}) )
assume A47: u in U19 ; :: thesis: u in union (Gg \ {U19})
Uk in Gg \ {U19} by A34, A38, A43, ZFMISC_1:64;
hence u in union (Gg \ {U19}) by A45, A47, TARSKI:def 4; :: thesis: verum

end;

hence contradiction by A24, A26; :: thesis: verum

end;

then UA c= sup D by YELLOW_1:22;
then A48: UA <= sup D by YELLOW_1:3;
D is directed by A7, A30, Th25;
then consider d being Element of (InclPoset the topology of L) such that
A49: d in D and
A50: UA <= d by A15, A48, WAYBEL_3:def 1;
consider u being Element of L such that
A51: d = (downarrow u) ` and
A52: u in U19 by A49;
U1 c= UA by A19, A26, A27, ZFMISC_1:92;
then A53: u in UA by A52;
A54: u <= u ;
UA c= d by A50, YELLOW_1:3;
then not u in downarrow u by A51, A53, XBOOLE_0:def 5;
hence contradiction by A54, WAYBEL_0:17; :: thesis: verum

end;

then uparrow (inf U19) c= U19 by A30, WAYBEL11:42;
then A55: U19 = uparrow (inf U19) by A28, XBOOLE_0:def 10;
take V = uparrow (inf U19); :: thesis: ( V in Bx & V c= S )
U19 is open by A7, A1, PRE_TOPC:def 5;
then U19 is Open by A8, A30, WAYBEL11:46;
then inf U19 is compact by A55, WAYBEL_8:2;
then inf U19 in the carrier of (CompactSublatt L) by WAYBEL_8:def 1;
then uparrow (inf U19) in B ;
hence V in Bx by A25, A28; :: thesis: V c= S
U1 c= UA by A21, A23, A26, ZFMISC_1:92;
hence V c= S by A55, A16, XBOOLE_1:1; :: thesis: verum

end;

hence Bx is Basis of x by A90; :: thesis: verum

end;

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

proof

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

end;

end;

then reconsider B = B as Basis of L by A4, YELLOW_8:23;
take B ; :: thesis: B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) }
thus B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } ; :: thesis: verum