set S0 = sqrt_0 0_No;
A1: L_ (sqrt_0 0_No) = {}

proof

assume L_ (sqrt_0 0_No) <> {} ; :: thesis: contradiction
then consider o being object such that
A2: o in L_ (sqrt_0 0_No) by XBOOLE_0:def 1;
consider l being Surreal such that
A3: ( o = sqrt l & l in L_ (NonNegativePart 0_No) ) by A2, Def9;
l in L_ 0_No by A3, Th2;
hence contradiction ; :: thesis: verum

end;

A4: R_ (sqrt_0 0_No) = {}

proof

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

end;

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

proof

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

end;

hence sqrt 0_No = 0_No by A1, A4, Th25; :: thesis: verum