let x be Surreal; :: thesis: ( x <= 0_No implies sqrt x is surreal )
assume A1: x <= 0_No ; :: thesis: sqrt x is surreal
A2: L_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in L_ (sqrt_0 x) or o is surreal )
assume o in L_ (sqrt_0 x) ; :: thesis: o is surreal
then consider l being Surreal such that
A3: ( o = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
0_No <= l by A3, Th2;
hence o is surreal by A3, Th19; :: thesis: verum

end;

R_ (sqrt_0 x) is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis: ( not o in R_ (sqrt_0 x) or o is surreal )
assume o in R_ (sqrt_0 x) ; :: thesis: o is surreal
then consider l being Surreal such that
A4: ( o = sqrt l & l in R_ (NonNegativePart x) ) by Def9;
0_No <= l by A4, Th2;
hence o is surreal by A4, Th19; :: thesis: verum

end;

then ( Union (sqrtR ((sqrt_0 x),x)) is surreal-membered & Union (sqrtL ((sqrt_0 x),x)) is surreal-membered ) by A2, Th10;
then consider M being Ordinal such that
A5: for o being object st o in (Union (sqrtL ((sqrt_0 x),x))) \/ (Union (sqrtR ((sqrt_0 x),x))) holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
Union (sqrtL ((sqrt_0 x),x)) << Union (sqrtR ((sqrt_0 x),x)) by A1, Th18;
then [(Union (sqrtL ((sqrt_0 x),x))),(Union (sqrtR ((sqrt_0 x),x)))] in Day M by A5, SURREAL0:46;
hence sqrt x is surreal by Th15; :: thesis: verum