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
set IPs = InclPoset the topology of L;
A3: sigma L = the topology of L by Th23;
A4: the carrier of (InclPoset the topology of L) = the topology of L by YELLOW_1:1;
set IU = { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ;
set y = "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L;

now

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 & x in V & V in sigma L ) ;
b is_<=_than V by A5, YELLOW_0:33;
hence b <= x by A5, 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 A6: "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L <= x by YELLOW_0:32;
assume A7: x <> "\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L ; :: thesis: contradiction
set VVl = (downarrow ("\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) ` ;

now

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 A6, A7, ORDERS_2:25; :: thesis: verum

end;

then A8: 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
A9: ( x in Vp & Vp in waybelow VVp ) by A8, TARSKI:def 4;
reconsider Vp = Vp as Element of (InclPoset the topology of L) by A9;
A10: Vp << VVp by A9, WAYBEL_3:7;
Vp in sigma L by A3, A4;
then reconsider Vl = Vp as Subset of L ;
consider bas being Basis of x such that
A11: for Y being Subset of L st Y in bas holds
( Y is open & Y is filtered ) by A1;
Vl is open by A4, PRE_TOPC:def 5;
then consider Ul being Subset of L such that
A12: ( Ul in bas & Ul c= Vl ) by A9, YELLOW_8:def 2;
A13: ( Ul is open & x in Ul ) by A12, YELLOW_8:21;
then Ul in sigma L by A3, PRE_TOPC:def 5;
then A14: inf Ul in { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } by A13;
"\/" { (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;
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 A15: (downarrow ("\/" { (inf V) where V is Subset of L : ( x in V & V in sigma L ) } ,L)) ` c= (downarrow (inf Ul)) ` by SUBSET_1:31;
set F = { (downarrow u) where u is Element of L : u in Ul } ;
A16: downarrow x in { (downarrow u) where u is Element of L : u in Ul } by A13;
{ (downarrow u) where u is Element of L : u in Ul } c= bool the carrier of L

proof

let X be set ; :: 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 consider u being Element of L such that
A17: ( X = downarrow u & u in Ul ) ;
thus X in bool the carrier of L by A17; :: 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 A16;
downarrow (inf Ul) = meet F by A13, Th15;
then A18: (downarrow (inf Ul)) ` = union (COMPLEMENT F) by TOPS_2:12;
A19: Ul is filtered by A11, A12;
A20: (downarrow x) ` in COMPLEMENT F by A16, YELLOW_8:14;
COMPLEMENT F c= the topology of L

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in COMPLEMENT F or X in the topology of L )
assume A21: X in COMPLEMENT F ; :: thesis: X in the topology of L
then reconsider X' = X as Subset of L ;
X' ` in F by A21, SETFAM_1:def 8;
then consider u being Element of L such that
A22: ( X' ` = downarrow u & u in Ul ) ;
X' = (downarrow u) ` by A22;
then X' is open by WAYBEL11:12;
hence X in the topology of L by PRE_TOPC:def 5; :: thesis: verum

end;

then reconsider CF = COMPLEMENT F as Subset of (InclPoset the topology of L) by YELLOW_1:1;
A23: CF is directed by A3, A19, Lm2;
VVp c= sup CF by A15, A18, YELLOW_1:22;
then VVp <= sup CF by YELLOW_1:3;
then consider d being Element of (InclPoset the topology of L) such that
A24: ( d in CF & Vp << d ) by A2, A3, A10, A20, A23, WAYBEL_4:54;
d in sigma L by A3, A4;
then reconsider d' = d as Subset of L ;
d' ` in F by A24, SETFAM_1:def 8;
then consider u being Element of L such that
A25: ( d' ` = downarrow u & u in Ul ) ;
Vp <= d by A24, WAYBEL_3:1;
then A26: Vp c= d by YELLOW_1:3;
u <= u ;
then u in downarrow u by WAYBEL_0:17;
then not u in Vp by A25, A26, XBOOLE_0:def 5;
hence contradiction by A12, A25; :: thesis: verum