theorem Th61: :: YELLOW_0:61

for L being non empty RelStr
for S being non empty full SubRelStr of L
for X being set
for a being Element of L
for x being Element of S st x = a holds
( ( a is_<=_than X implies x is_<=_than X ) & ( a is_>=_than X implies x is_>=_than X ) )