let L be lower-bounded continuous Scott TopLattice; :: thesis: for p being Element of L holds { () where q is Element of L : q << p } is Basis of
let p be Element of L; :: thesis: { () where q is Element of L : q << p } is Basis of
set X = { () 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 object ; :: according to TARSKI:def 3 :: thesis: ( not e in { () where q is Element of L : q << p } or e in bool the carrier of L )
assume e in { () 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 = { () where q is Element of L : q << p } as Subset-Family of L ;
X is Basis of
proof
A1: X is open
proof
let e be Subset of L; :: according to TOPS_2:def 1 :: thesis: ( not e in X or e is open )
assume e in X ; :: thesis: e is open
then consider q being Element of L such that
A2: e = wayabove q and
q << p ;
wayabove q is open by Lm11;
hence e is open by A2; :: thesis: verum
end;
X is p -quasi_basis
proof
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:43; :: according to YELLOW_8:def 1 :: thesis: for b1 being Element of K32( the carrier of L) holds
( not b1 is open or not p in b1 or ex b2 being Element of K32( the carrier of L) st
( b2 in X & b2 c= b1 ) )

let S be Subset of L; :: thesis: ( not S is open or not p in S or ex b1 being Element of K32( the carrier of L) st
( b1 in X & b1 c= S ) )

assume that
A3: S is open and
A4: p in S ; :: thesis: ex b1 being Element of K32( the carrier of L) st
( b1 in X & b1 c= S )

consider u being Element of L such that
A5: u << p and
A6: u in S by A3, A4, Lm10;
take V = wayabove u; :: thesis: ( V in X & V c= S )
thus V in X by A5; :: thesis: V c= S
A7: S is upper by ;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by ;
hence V c= S by A8; :: thesis: verum
end;
hence X is Basis of by A1; :: thesis: verum
end;
hence { (wayabove q) where q is Element of L : q << p } is Basis of ; :: thesis: verum