theorem Th21: :: WAYBEL32:21

for R being non empty TopRelStr
for A being Subset of R st ( for x being Element of R holds downarrow x = Cl {x} ) & A is open holds
A is upper