theorem Th9: :: WAYBEL_6:9

for L being complete LATTICE
for X being upper Open Subset of L
for x being Element of L st x in X ` holds
ex m being Element of L st
( x <= m & m is_maximal_in X ` )