theorem Th23: :: WAYBEL_0:23

for L being RelStr
for X being Subset of L holds
( X is lower iff downarrow X c= X )