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 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 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 object ; :: 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 2; :: 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 :: thesis: for x being Point of L ex Bx being Basis of x st Bx c= B

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

A9: 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 2; :: thesis: verum

end;

Bx is x -quasi_basis

proof

now :: thesis: x in Intersect Bx

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

end;

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

A11: now :: thesis: for Y being set st Y in Bx holds
x in Y

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 A10, SETFAM_1:def 9;
hence x in Intersect Bx by A10, A11, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

hence x in Intersect Bx ; :: 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 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
A12: S is open and
A13: 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, A12, PRE_TOPC:def 2;
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
A14: x in UA and
A15: UA in compactbelow S9 by A13, TARSKI:def 4;
reconsider UA = UA as Element of (InclPoset the topology of L) by A15;
UA is compact by A15, WAYBEL_8:4;
then A16: UA << UA ;
UA in the topology of L by A7, A1;
then reconsider UA9 = UA as Subset of L ;
UA <= S9 by A15, WAYBEL_8:4;
then A17: UA c= S by YELLOW_1:3;
consider F being Subset of (InclPoset (sigma L)) such that
A18: UA = sup F and
A19: 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;
A20: UA = union F by A7, A18, YELLOW_1:22;
F9 is open by A7, A1, PRE_TOPC:def 2;
then consider G being finite Subset of F9 such that
A21: UA c= union G by A20, A16, WAYBEL_3:34;
union G c= union F by ZFMISC_1:77;
then A22: UA = union G by A20, A21;
reconsider G = G as finite Subset-Family of L by XBOOLE_1:1;
consider Gg being finite Subset-Family of L such that
A23: Gg c= G and
A24: union Gg = union G and
A25: 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
A26: x in U1 and
A27: U1 in Gg by A14, A21, A24, TARSKI:def 4;
A28: Gg c= F by A23, XBOOLE_1:1;
then U1 in F by A27;
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;
A29: U19 c= uparrow (inf U19)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in U19 or x in uparrow (inf U19) )
assume A30: 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 A30, LATTICE3:def 8;
hence x in uparrow (inf U19) by WAYBEL_0:18; :: thesis: verum

end;

U1 is co-prime by A19, A27, A28;
then A31: ( U19 is filtered & U19 is upper ) by Th27;

now :: thesis: inf U19 in U19

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

proof

let d be object ; :: 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
A33: d = (downarrow u) ` and
u in U19 ;
(downarrow u) ` is open by WAYBEL11:12;
hence d in the topology of L by A33, PRE_TOPC:def 2; :: thesis: verum

end;

consider u being set such that
A34: u in U19 by A26;
reconsider u = u as Element of L by A34;
(downarrow u) ` in { ((downarrow u) `) where u is Element of L : u in U19 } by A34;
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 A32, YELLOW_1:1;
assume A35: not inf U19 in U19 ; :: thesis: contradiction

now :: thesis: UA c= union D

assume not UA c= union D ; :: thesis: contradiction
then consider l being object such that
A36: l in UA9 and
A37: not l in union D ;
reconsider l = l as Element of L by A36;
consider Uk being set such that
A38: l in Uk and
A39: Uk in Gg by A21, A24, A36, TARSKI:def 4;
A40: Gg c= F by A23, XBOOLE_1:1;
then Uk in F by A39;
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 A19, A39, A40;
then A41: ( Uk9 is filtered & Uk9 is upper ) by Th27;

now :: thesis: l is_<=_than U19

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

end;

then l <= inf U19 by YELLOW_0:33;
then A44: inf U19 in Uk9 by A38, A41;
A45: inf U19 is_<=_than U19 by YELLOW_0:33;
A46: U19 c= Uk

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in U19 or u in Uk )
assume A47: u in U19 ; :: thesis: u in Uk
then reconsider d = u as Element of L ;
inf U19 <= d by A45, A47, LATTICE3:def 8;
hence u in Uk by A41, A44; :: thesis: verum

end;

U19 c= union (Gg \ {U19})

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in U19 or u in union (Gg \ {U19}) )
assume A48: u in U19 ; :: thesis: u in union (Gg \ {U19})
Uk in Gg \ {U19} by A35, A39, A44, ZFMISC_1:56;
hence u in union (Gg \ {U19}) by A46, A48, TARSKI:def 4; :: thesis: verum

end;

hence contradiction by A25, A27; :: thesis: verum

end;

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

end;

then uparrow (inf U19) c= U19 by A31, WAYBEL11:42;
then A56: U19 = uparrow (inf U19) by A29;
take V = uparrow (inf U19); :: thesis: ( V in Bx & V c= S )
U19 is open by A7, A1, PRE_TOPC:def 2;
then U19 is Open by A8, A31, WAYBEL11:46;
then inf U19 is compact by A56, 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 A26, A29; :: thesis: V c= S
U1 c= UA by A22, A24, A27, ZFMISC_1:74;
hence V c= S by A56, A17; :: thesis: verum

end;

hence Bx is Basis of x by A9; :: 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 object ; :: 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:14;
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