for T being non empty TopSpace
for X being Subset of (Domains_Lattice T) ex a being Element of (Domains_Lattice T) st
( X is_less_than a & ( for b being Element of (Domains_Lattice T) st X is_less_than b holds
a [= b ) )