let L be complete Scott TopLattice; :: thesis: for x being Element of L st L is continuous holds
ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
let x be Element of L; :: thesis: ( L is continuous implies ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) )
assume A1: L is continuous ; :: thesis: ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered )
then reconsider A = { (wayabove q) where q is Element of L : q << x } as Basis of x by WAYBEL11:44;
set B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ;
{ V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } c= bool the carrier of L

proof

let X be set ; :: according to TARSKI:def 3 :: thesis: ( not X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } or X in bool the carrier of L )
assume X in { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } ; :: thesis: X in bool the carrier of L
then ex V being Subset of L st
( X = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
hence X in bool the carrier of L ; :: thesis: verum

end;

then reconsider B = { V where V is Subset of L : ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) } as Subset-Family of L ;
reconsider B = B as Subset-Family of L ;
A2: B is Basis of x

proof

thus B c= the topology of L :: according to YELLOW_8:def 2 :: thesis: ( x in Intersect B & ( 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 B & b₂ c= b₁ ) ) ) )

proof

let Y be set ; :: according to TARSKI:def 3 :: thesis: ( not Y in B or Y in the topology of L )
assume Y in B ; :: thesis: Y in the topology of L
then consider V being Subset of L such that
A3: ( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
thus Y in the topology of L by A3, PRE_TOPC:def 5; :: thesis: verum

end;

thus x in Intersect B :: 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 B & b₂ c= b₁ ) )

proof

per cases ( B is empty or not B is empty ) ;

suppose B is empty ; :: thesis: x in Intersect B

then Intersect B = the carrier of L by SETFAM_1:def 10;
hence x in Intersect B ; :: thesis: verum

end;

suppose A4: not B is empty ; :: thesis: x in Intersect B

then A5: Intersect B = meet B by SETFAM_1:def 10;

now

let Y be set ; :: thesis: ( Y in B implies x in Y )
assume Y in B ; :: thesis: x in Y
then consider V being Subset of L such that
A6: ( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
thus x in Y by A6; :: thesis: verum

end;

hence x in Intersect B by A4, A5, SETFAM_1:def 1; :: thesis: verum

end;

end;

end;

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 B & b₁ c= S ) )
assume ( S is open & x in S ) ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in B & b₁ c= S )
then consider V being Subset of L such that
A7: ( V in A & V c= S ) by YELLOW_8:def 2;
consider q being Element of L such that
A8: ( V = wayabove q & q << x ) by A7;
consider F being Open Filter of L such that
A9: ( x in F & F c= wayabove q ) by A1, A8, WAYBEL_6:8;
take F ; :: thesis: ( F in B & F c= S )
F is open by WAYBEL11:41;
hence F in B by A8, A9; :: thesis: F c= S
thus F c= S by A7, A8, A9, XBOOLE_1:1; :: thesis: verum

end;

now

let Y be Subset of L; :: thesis: ( Y in B implies ( Y is open & Y is filtered ) )
assume Y in B ; :: thesis: ( Y is open & Y is filtered )
then consider V being Subset of L such that
A10: ( Y = V & ex q being Element of L st
( V c= wayabove q & q << x & x in V & V is open & V is filtered ) ) ;
thus ( Y is open & Y is filtered ) by A10; :: thesis: verum

end;

hence ex B being Basis of x st
for X being Subset of L st X in B holds
( X is open & X is filtered ) by A2; :: thesis: verum