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