theorem :: YELLOW_0:9

for L being RelStr
for X, Y being set st X c= Y holds
for x being Element of L holds
( ( x is_<=_than Y implies x is_<=_than X ) & ( x is_>=_than Y implies x is_>=_than X ) ) ;