let T be complete 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
proof
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 Th36;
hence e in the topology of T by A2; :: thesis: verum
end;
then reconsider P = { (wayabove x) where x is Element of T : verum } as Subset-Family of T by XBOOLE_1:1;
for x being Point of T ex B being Basis of st B c= P
proof
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 Th44;
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;
hence { (wayabove x) where x is Element of T : verum } is Basis of T by A1, YELLOW_8:14; :: thesis: verum