for L being non empty RelStr
for X being set
for x being Element of L holds
( ( x is_>=_than X implies x is_>=_than X /\ the carrier of L ) & ( x is_>=_than X /\ the carrier of L implies x is_>=_than X ) & ( x is_<=_than X implies x is_<=_than X /\ the carrier of L ) & ( x is_<=_than X /\ the carrier of L implies x is_<=_than X ) )