theorem :: WAYBEL_6:6

for L being up-complete LATTICE
for X being upper Subset of L holds
( X is Open iff X = union { (wayabove x) where x is Element of L : x in X } )