let L be complete Scott TopLattice; :: thesis: ( ex B being Basis of L st B = { (uparrow x) where x is Element of L : x in the carrier of (CompactSublatt L) } implies ( 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 ) ) ) ) )
given B being Basis of L such that A1: B = { (uparrow k) where k is Element of L : k in the carrier of (CompactSublatt L) } ; :: 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 ) ) ) )
set IPs = InclPoset (sigma L);
set IPt = InclPoset the topology of L;
A2: the carrier of (InclPoset (sigma L)) = sigma L by YELLOW_1:1;
A3: sigma L = the topology of L by Th23;
A4: InclPoset (sigma L) = InclPoset the topology of L by Th23;
thus InclPoset (sigma L) is algebraic :: thesis: 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 ) )
proof
thus for X being Element of (InclPoset (sigma L)) holds
( not compactbelow X is empty & compactbelow X is directed ) by A3; :: according to WAYBEL_8:def 4 :: thesis: ( InclPoset (sigma L) is up-complete & InclPoset (sigma L) is satisfying_axiom_K )
thus InclPoset (sigma L) is up-complete by A4; :: thesis: InclPoset (sigma L) is satisfying_axiom_K
let X be Element of (InclPoset (sigma L)); :: according to WAYBEL_8:def 3 :: thesis: X = "\/" ((compactbelow X),(InclPoset (sigma L)))
set cX = compactbelow X;
set GB = { G where G is Subset of L : ( G in B & G c= X ) } ;
X in sigma L by A2;
then reconsider X9 = X as Subset of L ;
X9 is open by A2, Th24;
then A5: X = union { G where G is Subset of L : ( G in B & G c= X ) } by YELLOW_8:9;
A6: now :: thesis: for x being object holds
( ( x in X implies x in union (compactbelow X) ) & ( x in union (compactbelow X) implies x in X ) )
let x be object ; :: thesis: ( ( x in X implies x in union (compactbelow X) ) & ( x in union (compactbelow X) implies x in X ) )
hereby :: thesis: ( x in union (compactbelow X) implies x in X )
assume x in X ; :: thesis: x in union (compactbelow X)
then consider GG being set such that
A7: x in GG and
A8: GG in { G where G is Subset of L : ( G in B & G c= X ) } by A5, TARSKI:def 4;
consider G being Subset of L such that
A9: G = GG and
A10: G in B and
A11: G c= X by A8;
consider k being Element of L such that
A12: G = uparrow k and
A13: k in the carrier of (CompactSublatt L) by A1, A10;
k is compact by A13, WAYBEL_8:def 1;
then uparrow k is Open by WAYBEL_8:2;
then uparrow k is open by WAYBEL11:41;
then reconsider G = G as Element of (InclPoset (sigma L)) by A3, A2, A12, PRE_TOPC:def 2;
for X being Subset of L st X is open holds
X is upper by WAYBEL11:def 4;
then uparrow k is compact by Th22;
then A14: G is compact by A3, A12, WAYBEL_3:36;
G <= X by A11, YELLOW_1:3;
then G in compactbelow X by A14;
hence x in union (compactbelow X) by A7, A9, TARSKI:def 4; :: thesis: verum
end;
assume x in union (compactbelow X) ; :: thesis: x in X
then consider G being set such that
A15: x in G and
A16: G in compactbelow X by TARSKI:def 4;
reconsider G = G as Element of (InclPoset (sigma L)) by A16;
G <= X by A16, WAYBEL_8:4;
then G c= X by YELLOW_1:3;
hence x in X by A15; :: thesis: verum
end;
sup (compactbelow X) = union (compactbelow X) by A3, YELLOW_1:22;
hence X = "\/" ((compactbelow X),(InclPoset (sigma L))) by A6, TARSKI:2; :: thesis: verum
end;
let V be Element of (InclPoset (sigma L)); :: thesis: 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 ) )
V in sigma L by A2;
then reconsider V9 = V as Subset of L ;
set GB = { G where G is Subset of L : ( G in B & G c= V ) } ;
{ G where G is Subset of L : ( G in B & G c= V ) } c= the carrier of (InclPoset (sigma L))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { G where G is Subset of L : ( G in B & G c= V ) } or x in the carrier of (InclPoset (sigma L)) )
assume x in { G where G is Subset of L : ( G in B & G c= V ) } ; :: thesis: x in the carrier of (InclPoset (sigma L))
then consider G being Subset of L such that
A17: G = x and
A18: G in B and
G c= V ;
G is open by A18, YELLOW_8:10;
hence x in the carrier of (InclPoset (sigma L)) by A2, A17, Th24; :: thesis: verum
end;
then reconsider GB = { G where G is Subset of L : ( G in B & G c= V ) } as Subset of (InclPoset (sigma L)) ;
take GB ; :: thesis: ( V = sup GB & ( for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime ) )
V9 is open by A2, Th24;
then V = union GB by YELLOW_8:9;
hence V = sup GB by A3, YELLOW_1:22; :: thesis: for W being Element of (InclPoset (sigma L)) st W in GB holds
W is co-prime
let x be Element of (InclPoset (sigma L)); :: thesis: ( x in GB implies x is co-prime )
assume x in GB ; :: thesis: x is co-prime
then consider G being Subset of L such that
A19: G = x and
A20: G in B and
G c= V ;
ex k being Element of L st
( G = uparrow k & k in the carrier of (CompactSublatt L) ) by A1, A20;
hence x is co-prime by A19, Th27; :: thesis: verum