let L be complete Scott TopLattice; :: thesis: for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)
let x be Element of L; :: thesis: ( ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous implies x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L) )
assume that
A1: for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) and
A2: InclPoset (sigma L) is continuous ; :: thesis: x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)
A3: sigma L = the topology of L by Th23;
set IU = { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ;
set IPs = InclPoset the topology of L;
A4: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
set y = "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L);
set VVl = (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` ;
now :: thesis: for b being Element of L st b in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } holds
b <= x
let b be Element of L; :: thesis: ( b in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } implies b <= x )
assume b in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ; :: thesis: b <= x
then consider V being Subset of L such that
A5: b = inf V and
A6: x in V and
V in sigma L ;
b is_<=_than V by A5, YELLOW_0:33;
hence b <= x by A6, LATTICE3:def 8; :: thesis: verum
end;
then x is_>=_than { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by LATTICE3:def 9;
then A7: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) <= x by YELLOW_0:32;
assume A8: x <> "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) ; :: thesis: contradiction
now :: thesis: not x in downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))
assume x in downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) ; :: thesis: contradiction
then x <= "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by WAYBEL_0:17;
hence contradiction by A7, A8, ORDERS_2:2; :: thesis: verum
end;
then A9: x in (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` by XBOOLE_0:def 5;
(downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` is open by WAYBEL11:12;
then reconsider VVp = (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` as Element of (InclPoset the topology of L) by A3, A4, Th24;
VVp = sup (waybelow VVp) by A2, A3, WAYBEL_3:def 5;
then VVp = union (waybelow VVp) by YELLOW_1:22;
then consider Vp being set such that
A10: x in Vp and
A11: Vp in waybelow VVp by A9, TARSKI:def 4;
reconsider Vp = Vp as Element of (InclPoset the topology of L) by A11;
Vp in sigma L by A3, A4;
then reconsider Vl = Vp as Subset of L ;
A12: Vp << VVp by A11, WAYBEL_3:7;
consider bas being Basis of x such that
A13: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A1;
A14: "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) is_>=_than { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by YELLOW_0:32;
Vl is open by A4, PRE_TOPC:def 2;
then consider Ul being Subset of L such that
A15: Ul in bas and
A16: Ul c= Vl by A10, YELLOW_8:def 1;
set F = { (downarrow u) where u is Element of L : u in Ul } ;
A17: x in Ul by A15, YELLOW_8:12;
then A18: downarrow x in { (downarrow u) where u is Element of L : u in Ul } ;
{ (downarrow u) where u is Element of L : u in Ul } c= bool the carrier of L
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in { (downarrow u) where u is Element of L : u in Ul } or X in bool the carrier of L )
assume X in { (downarrow u) where u is Element of L : u in Ul } ; :: thesis: X in bool the carrier of L
then ex u being Element of L st
( X = downarrow u & u in Ul ) ;
hence X in bool the carrier of L ; :: thesis: verum
end;
then reconsider F = { (downarrow u) where u is Element of L : u in Ul } as non empty Subset-Family of L by A18;
COMPLEMENT F c= the topology of L
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in COMPLEMENT F or X in the topology of L )
assume A19: X in COMPLEMENT F ; :: thesis: X in the topology of L
then reconsider X9 = X as Subset of L ;
X9 ` in F by A19, SETFAM_1:def 7;
then consider u being Element of L such that
A20: X9 ` = downarrow u and
u in Ul ;
X9 = (downarrow u) ` by A20;
then X9 is open by WAYBEL11:12;
hence X in the topology of L by PRE_TOPC:def 2; :: thesis: verum
end;
then reconsider CF = COMPLEMENT F as Subset of (InclPoset the topology of L) by YELLOW_1:1;
Ul is filtered by A13, A15;
then A21: CF is directed by A3, Lm2;
Ul is open by A15, YELLOW_8:12;
then Ul in sigma L by A3, PRE_TOPC:def 2;
then inf Ul in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by A17;
then inf Ul <= "\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L) by A14, LATTICE3:def 9;
then downarrow (inf Ul) c= downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) by WAYBEL_0:21;
then A22: (downarrow ("\/" ( { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L))) ` c= (downarrow (inf Ul)) ` by SUBSET_1:12;
downarrow (inf Ul) = meet F by A17, Th15;
then (downarrow (inf Ul)) ` = union (COMPLEMENT F) by TOPS_2:7;
then VVp c= sup CF by A22, YELLOW_1:22;
then A23: VVp <= sup CF by YELLOW_1:3;
(downarrow x) ` in COMPLEMENT F by A18, YELLOW_8:5;
then consider d being Element of (InclPoset the topology of L) such that
A24: d in CF and
A25: Vp << d by A2, A3, A12, A21, A23, WAYBEL_4:53;
Vp <= d by A25, WAYBEL_3:1;
then A26: Vp c= d by YELLOW_1:3;
d in sigma L by A3, A4;
then reconsider d9 = d as Subset of L ;
d9 ` in F by A24, SETFAM_1:def 7;
then consider u being Element of L such that
A27: d9 ` = downarrow u and
A28: u in Ul ;
u <= u ;
then u in downarrow u by WAYBEL_0:17;
then not u in Vp by A27, A26, XBOOLE_0:def 5;
hence contradiction by A16, A28; :: thesis: verum