theorem :: SURREALS:13

for o being object
for p being pair object holds Union (sqrtR (p,o)) = ((R_ p) \/ (sqrt (o,(Union (sqrtL (p,o))),(Union (sqrtL (p,o)))))) \/ (sqrt (o,(Union (sqrtR (p,o))),(Union (sqrtR (p,o)))))