theorem Th25: :: SURREALS:25

for x being Surreal st ( for y being Surreal st y in (L_ (NonNegativePart x)) \/ (R_ (NonNegativePart x)) holds
y == 0_No ) holds
sqrt x = sqrt_0 x