let o be object ; :: thesis: for p being pair object st L_ p is surreal-membered & R_ p is surreal-membered holds
( Union (sqrtL (p,o)) is surreal-membered & Union (sqrtR (p,o)) is surreal-membered )
let p be pair object ; :: thesis: ( L_ p is surreal-membered & R_ p is surreal-membered implies ( Union (sqrtL (p,o)) is surreal-membered & Union (sqrtR (p,o)) is surreal-membered ) )
assume A1: ( L_ p is surreal-membered & R_ p is surreal-membered ) ; :: thesis: ( Union (sqrtL (p,o)) is surreal-membered & Union (sqrtR (p,o)) is surreal-membered )
thus Union (sqrtL (p,o)) is surreal-membered :: thesis: Union (sqrtR (p,o)) is surreal-membered

proof

let a be object ; :: according to SURREAL0:def 16 :: thesis: ( not a in Union (sqrtL (p,o)) or a is surreal )
assume a in Union (sqrtL (p,o)) ; :: thesis: a is surreal
then consider n being object such that
A2: ( n in dom (sqrtL (p,o)) & a in (sqrtL (p,o)) . n ) by CARD_5:2;
dom (sqrtL (p,o)) = NAT by Def4;
then reconsider n = n as Nat by A2;
(sqrtL (p,o)) . n is surreal-membered by A1, Th9;
hence a is surreal by A2; :: thesis: verum

end;

let a be object ; :: according to SURREAL0:def 16 :: thesis: ( not a in Union (sqrtR (p,o)) or a is surreal )
assume a in Union (sqrtR (p,o)) ; :: thesis: a is surreal
then consider n being object such that
A3: ( n in dom (sqrtR (p,o)) & a in (sqrtR (p,o)) . n ) by CARD_5:2;
dom (sqrtR (p,o)) = NAT by Def5;
then reconsider n = n as Nat by A3;
(sqrtR (p,o)) . n is surreal-membered by A1, Th9;
hence a is surreal by A3; :: thesis: verum