for L being up-complete LATTICE
for X being upper Subset of L holds
( X is Open iff for x being Element of L st x in X holds
waybelow x meets X )