theorem Th4: :: YELLOW_0:4

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