let L be complete Scott TopLattice; :: thesis: ( InclPoset (sigma L) is algebraic & ( for V being Element of ex VV being Subset of st
( V = sup VV & ( for W being Element of 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 : 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 : k in the carrier of (CompactSublatt L) } ;
{ (uparrow k) where k is Element of : 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 : 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 : k in the carrier of (CompactSublatt L) } ; :: thesis: x in bool the carrier of L
then ex k being Element of 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 : k in the carrier of (CompactSublatt L) } as Subset-Family of ;
assume that
A2: InclPoset (sigma L) is algebraic and
A3: for V being Element of ex X being Subset of st
( V = sup X & ( for x being Element of 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 : 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 ;
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 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 ex X being Basis of x st
for Y being Subset of st Y in X holds
( Y is open & Y is filtered ) ) ) by A3, Th39;
then for x being Element of holds x = "\/" { (inf V) where V is Subset of : ( x in V & V in sigma L ) } ,L by Th37;
then A8: L is continuous by Th38;

now

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

proof

A90: Bx is open

proof

let y be Subset of ; :: 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 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 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 ; :: 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 S' = S as Element of by A7, A1, A11, PRE_TOPC:def 5;
S' = sup (compactbelow S') by A2, A7, WAYBEL_8:def 3;
then S' = union (compactbelow S') by YELLOW_1:22;
then consider UA being set such that
A13: x in UA and
A14: UA in compactbelow S' by A12, TARSKI:def 4;
reconsider UA = UA as Element of 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 UA' = UA as Subset of ;
UA <= S' by A14, WAYBEL_8:4;
then A16: UA c= S by YELLOW_1:3;
consider F being Subset of such that
A17: UA = sup F and
A18: for x being Element of st x in F holds
x is co-prime by A3, A7;
reconsider F' = F as Subset-Family of by A1, XBOOLE_1:1;
A19: UA = union F by A7, A17, YELLOW_1:22;
F' is open

proof

let P be Subset of ; :: according to TOPS_2:def 1 :: thesis: ( not P in F' or P is open )
assume P in F' ; :: 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 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 by XBOOLE_1:1;
consider Gg being finite Subset-Family of such that
A22: Gg c= G and
A23: union Gg = union G and
A24: for g being Subset of 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 ;
U1 in the topology of L by A7, A1;
then reconsider U1' = U1 as Subset of ;
set k = inf U1';
A28: U1' c= uparrow (inf U1')

proof

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

end;

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

now

set D = { ((downarrow u) ` ) where u is Element of : u in U1' } ;
A31: { ((downarrow u) ` ) where u is Element of : u in U1' } 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 : u in U1' } or d in the topology of L )
assume d in { ((downarrow u) ` ) where u is Element of : u in U1' } ; :: thesis: d in the topology of L
then consider u being Element of such that
A32: d = (downarrow u) ` and
u in U1' ;
(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 U1' by A25;
reconsider u = u as Element of by A33;
(downarrow u) ` in { ((downarrow u) ` ) where u is Element of : u in U1' } by A33;
then reconsider D = { ((downarrow u) ` ) where u is Element of : u in U1' } as non empty Subset of by A31, YELLOW_1:1;
assume A34: not inf U1' in U1' ; :: thesis: contradiction

now

assume not UA c= union D ; :: thesis: contradiction
then consider l being set such that
A35: l in UA' and
A36: not l in union D by TARSKI:def 3;
reconsider l = l as Element of 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 ;
Uk in the topology of L by A7, A1;
then reconsider Uk' = Uk as Subset of ;
Uk is co-prime by A18, A38, A39;
then A40: ( Uk' is filtered & Uk' is upper ) by Th27;

now

assume not l is_<=_than U1' ; :: thesis: contradiction
then consider m being Element of such that
A41: m in U1' 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 U1' by YELLOW_0:33;
then A43: inf U1' in Uk' by A37, A40, WAYBEL_0:def 20;
A44: inf U1' is_<=_than U1' by YELLOW_0:33;
A45: U1' c= Uk

proof

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

end;

U1' c= union (Gg \ {U1'})

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in U1' or u in union (Gg \ {U1'}) )
assume A47: u in U1' ; :: thesis: u in union (Gg \ {U1'})
Uk in Gg \ {U1'} by A34, A38, A43, ZFMISC_1:64;
hence u in union (Gg \ {U1'}) 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 such that
A49: d in D and
A50: UA <= d by A15, A48, WAYBEL_3:def 1;
consider u being Element of such that
A51: d = (downarrow u) ` and
A52: u in U1' 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 U1') c= U1' by A30, WAYBEL11:42;
then A55: U1' = uparrow (inf U1') by A28, XBOOLE_0:def 10;
take V = uparrow (inf U1'); :: thesis: ( V in Bx & V c= S )
U1' is open by A7, A1, PRE_TOPC:def 5;
then U1' is Open by A8, A30, WAYBEL11:46;
then inf U1' is compact by A55, WAYBEL_8:2;
then inf U1' in the carrier of (CompactSublatt L) by WAYBEL_8:def 1;
then uparrow (inf U1') 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 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 : x in the carrier of (CompactSublatt L) }
thus B = { (uparrow x) where x is Element of : x in the carrier of (CompactSublatt L) } ; :: thesis: verum