theorem Th18: :: SURREALO:18
for X being set
for x, y being Surreal st {x} << X & y <= x holds
{y} << X