theorem Th15: :: SURREALS:15

for x being Surreal holds sqrt x = [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))]