theorem Th17: :: SURREALS:17

for x1, x2, y, z being Surreal st not x2 == 0_No & y = x1 * (x2 ") holds
( ( y * y < z implies x1 * x1 < z * (x2 * x2) ) & ( x1 * x1 < z * (x2 * x2) implies y * y < z ) & ( z < y * y implies z * (x2 * x2) < x1 * x1 ) & ( z * (x2 * x2) < x1 * x1 implies z < y * y ) )