let T be lower-bounded continuous Scott TopLattice; :: thesis: { () where x is Element of T : verum } is Basis of T
set B = { () 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 { () where x is Element of T : verum } or e in the topology of T )
assume e in { () 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;
then reconsider P = { () 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 = { () 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;
hence { (wayabove x) where x is Element of T : verum } is Basis of T by ; :: thesis: verum