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
let p be Element of L; :: thesis: { (wayabove q) where q is Element of L : q << p } is Basis of
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 object ; :: 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

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 b₁ being Element of K32( the carrier of L) holds
( not b₁ is open or not p in b₁ or ex b₂ being Element of K32( 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 K32( the carrier of L) st
( b₁ in X & b₁ c= S ) )
assume that
A3: S is open and
A4: p in S ; :: thesis: ex b₁ being Element of K32( the carrier of L) st
( b₁ in X & b₁ 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 A3, WAYBEL11:def 4;
A8: wayabove u c= uparrow u by WAYBEL_3:11;
uparrow u c= S by A6, A7, WAYBEL11:42;
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