for L being complete Scott TopLattice
for x being Element of L st ( for x being Element of L ex B being Basis of x st
for Y being Subset of L st Y in B holds
( Y is open & Y is filtered ) ) & InclPoset (sigma L) is continuous holds
x = "\/" ( { (inf X) where X is Subset of L : ( x in X & X in sigma L ) } ,L)