theorem :: SURREALS:12

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