theorem Th97: :: TDLAT_2:98

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