set S0 = sqrt_0 1_No;
( 0_No in L_ 1_No & 0_No <= 0_No ) by TARSKI:def 1;
then 0_No in L_ (NonNegativePart 1_No) by Def1;
then A7: sqrt 0_No in L_ (sqrt_0 1_No) by Def9;
L_ (sqrt_0 1_No) c= {0_No}

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in L_ (sqrt_0 1_No) or o in {0_No} )
assume o in L_ (sqrt_0 1_No) ; :: thesis: o in {0_No}
then consider l being Surreal such that
A8: ( o = sqrt l & l in L_ (NonNegativePart 1_No) ) by Def9;
l in L_ 1_No by A8, Th2;
then l = 0_No by TARSKI:def 1;
hence o in {0_No} by A8, TARSKI:def 1; :: thesis: verum

end;

then A9: L_ (sqrt_0 1_No) = {0_No} by A7, ZFMISC_1:33;
A10: R_ (sqrt_0 1_No) = {}

proof

assume R_ (sqrt_0 1_No) <> {} ; :: thesis: contradiction
then consider o being object such that
A11: o in R_ (sqrt_0 1_No) by XBOOLE_0:def 1;
consider r being Surreal such that
A12: ( o = sqrt r & r in R_ (NonNegativePart 1_No) ) by A11, Def9;
r in R_ 1_No by A12, Th2;
hence contradiction ; :: thesis: verum

end;

for y being Surreal st y in (L_ (NonNegativePart 1_No)) \/ (R_ (NonNegativePart 1_No)) holds
y == 0_No

proof

let y be Surreal; :: thesis: ( y in (L_ (NonNegativePart 1_No)) \/ (R_ (NonNegativePart 1_No)) implies y == 0_No )
assume y in (L_ (NonNegativePart 1_No)) \/ (R_ (NonNegativePart 1_No)) ; :: thesis: y == 0_No
then ( y in L_ (NonNegativePart 1_No) or y in R_ (NonNegativePart 1_No) ) by XBOOLE_0:def 3;
then ( y in L_ 1_No or y in R_ 1_No ) by Th2;
hence y == 0_No by TARSKI:def 1; :: thesis: verum

end;

hence sqrt 1_No = 1_No by A10, A9, Th25; :: thesis: verum