for L being complete Scott TopLattice
for x being Element of L
for X being Subset of L st X is open & x in X holds
inf X << x