let L be lower-bounded continuous Scott TopLattice; :: thesis: for p being Element of L holds { (wayabove q) where q is Element of L : q << p } is Basis of p
let p be Element of L; :: thesis: { (wayabove q) where q is Element of L : q << p } is Basis of p
set X = { (wayabove q) where q is Element of L : q << p } ;
{ (wayabove q) where q is Element of L : q << p } c= bool the carrier of L

proof

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

end;

then reconsider X = { (wayabove q) where q is Element of L : q << p } as Subset-Family of L ;
X is Basis of p

proof

thus X c= the topology of L :: according to YELLOW_8:def 2 :: thesis: ( p in Intersect X & ( for b₁ being Element of bool the carrier of L holds
( not b₁ is open or not p in b₁ or ex b₂ being Element of bool the carrier of L st
( b₂ in X & b₂ c= b₁ ) ) ) )

proof

let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in X or e in the topology of L )
assume e in X ; :: thesis: e in the topology of L
then consider q being Element of L such that
A1: e = wayabove q and
q << p ;
wayabove q is open by Lm11;
hence e in the topology of L by A1, PRE_TOPC:def 5; :: thesis: verum

end;

for Y being set st Y in X holds
p in Y

proof

let e be set ; :: thesis: ( e in X implies p in e )
assume e in X ; :: thesis: p in e
then ex q being Element of L st
( e = wayabove q & q << p ) ;
hence p in e ; :: thesis: verum

end;

hence p in Intersect X by SETFAM_1:58; :: thesis: for b₁ being Element of bool the carrier of L holds
( not b₁ is open or not p in b₁ or ex b₂ being Element of bool the carrier of L st
( b₂ in X & b₂ c= b₁ ) )
let S be Subset of L; :: thesis: ( not S is open or not p in S or ex b₁ being Element of bool the carrier of L st
( b₁ in X & b₁ c= S ) )
assume that
A2: S is open and
A3: p in S ; :: thesis: ex b₁ being Element of bool the carrier of L st
( b₁ in X & b₁ c= S )
consider u being Element of L such that
A4: u << p and
A5: u in S by A2, A3, Lm10;
take V = wayabove u; :: thesis: ( V in X & V c= S )
thus V in X by A4; :: thesis: V c= S
A6: S is upper by A2, WAYBEL11:def 4;
A7: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A5, A6, WAYBEL11:42;
hence V c= S by A7, XBOOLE_1:1; :: thesis: verum

end;

hence { (wayabove q) where q is Element of L : q << p } is Basis of p ; :: thesis: verum