for L being non empty reflexive transitive RelStr
for X being Subset of L
for x being Element of L holds
( x is_<=_than X iff x is_<=_than uparrow X )