let T be lower-bounded continuous Scott TopLattice; :: thesis: { (wayabove x) where x is Element of T : verum } is Basis of T

set B = { (wayabove x) where x is Element of T : verum } ;

A1: { (wayabove x) where x is Element of T : verum } c= the topology of T

for x being Point of T ex B being Basis of st B c= P

set B = { (wayabove x) where x is Element of T : verum } ;

A1: { (wayabove x) where x is Element of T : verum } c= the topology of T

proof

then reconsider P = { (wayabove x) where x is Element of T : verum } as Subset-Family of T by XBOOLE_1:1;
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in { (wayabove x) where x is Element of T : verum } or e in the topology of T )

assume e in { (wayabove x) where x is Element of T : verum } ; :: thesis: e in the topology of T

then consider x being Element of T such that

A2: e = wayabove x ;

wayabove x is open by Lm11;

hence e in the topology of T by A2; :: thesis: verum

end;assume e in { (wayabove x) where x is Element of T : verum } ; :: thesis: e in the topology of T

then consider x being Element of T such that

A2: e = wayabove x ;

wayabove x is open by Lm11;

hence e in the topology of T by A2; :: thesis: verum

for x being Point of T ex B being Basis of st B c= P

proof

hence
{ (wayabove x) where x is Element of T : verum } is Basis of T
by A1, YELLOW_8:14; :: thesis: verum
let x be Point of T; :: thesis: ex B being Basis of st B c= P

reconsider p = x as Element of T ;

reconsider A = { (wayabove q) where q is Element of T : q << p } as Basis of by Lm12;

take A ; :: thesis: A c= P

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in P )

assume u in A ; :: thesis: u in P

then ex q being Element of T st

( u = wayabove q & q << p ) ;

hence u in P ; :: thesis: verum

end;reconsider p = x as Element of T ;

reconsider A = { (wayabove q) where q is Element of T : q << p } as Basis of by Lm12;

take A ; :: thesis: A c= P

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in A or u in P )

assume u in A ; :: thesis: u in P

then ex q being Element of T st

( u = wayabove q & q << p ) ;

hence u in P ; :: thesis: verum