theorem Th15: :: WAYBEL_0:15

for L being non empty RelStr
for X being Subset of L holds uparrow X = { x where x is Element of L : ex y being Element of L st
( x >= y & y in X ) }