theorem Th9: :: YELLOW_7:9

for L being RelStr
for x being Element of (L opp)
for X being set holds
( ( x is_<=_than X implies ~ x is_>=_than X ) & ( ~ x is_>=_than X implies x is_<=_than X ) & ( x is_>=_than X implies ~ x is_<=_than X ) & ( ~ x is_<=_than X implies x is_>=_than X ) )