theorem :: SURREALS:30

for x being Surreal st 0_No < x holds
(sqrt x) " == sqrt (x ")