theorem Th62: :: YELLOW_0:62

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