theorem Th72: :: SURREALC:72
for x, y, z being Surreal
for r being Real
for s being Surreal st r <> 0 & x is s,y,r _term & x == z holds
z is s,y,r _term