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

X 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

then reconsider X = { (wayabove q) where q is Element of L : q << p } as Subset-Family of L ;
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;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

X is Basis of

proof

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

end;proof

X is p -quasi_basis
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;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

proof

hence
X is Basis of
by A1; :: thesis: verum
for Y being set st Y in X holds

p in Y_{1} being Element of K32( the carrier of L) holds

( not b_{1} is open or not p in b_{1} or ex b_{2} being Element of K32( the carrier of L) st

( b_{2} in X & b_{2} c= b_{1} ) )

let S be Subset of L; :: thesis: ( not S is open or not p in S or ex b_{1} being Element of K32( the carrier of L) st

( b_{1} in X & b_{1} c= S ) )

assume that

A3: S is open and

A4: p in S ; :: thesis: ex b_{1} being Element of K32( the carrier of L) st

( b_{1} in X & b_{1} 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;p in Y

proof

hence
p in Intersect X
by SETFAM_1:43; :: according to YELLOW_8:def 1 :: thesis: for b
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;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

( not b

( b

let S be Subset of L; :: thesis: ( not S is open or not p in S or ex b

( b

assume that

A3: S is open and

A4: p in S ; :: thesis: ex b

( b

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