theorem Th24: :: WAYBEL_0:24

for L being RelStr
for X being Subset of L holds
( X is upper iff uparrow X c= X )