theorem Th17: :: SURREALO:17

for X being set
for x, y being Surreal st X << {x} & x <= y holds
X << {y}