theorem :: SURREALC:12
for x, y, z being Surreal st x infinitely< y & y <= z holds
x infinitely< z by SURREALO:4;