let x be Surreal; :: thesis: ( x < 0_No & ( for y being Surreal st y in R_ x holds
y < 0_No ) implies sqrt x = 0_No )
assume that
A1: x < 0_No and
A2: for y being Surreal st y in R_ x holds
y < 0_No ; :: thesis: sqrt x = 0_No
defpred S₁[ Nat] means (sqrtR ((sqrt_0 x),x)) . $1 = {} ;
A3: S₁[ 0 ]

proof

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

end;

A6: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
assume (sqrtR ((sqrt_0 x),x)) . (n + 1) <> {} ; :: thesis: contradiction
then consider y being object such that
A8: y in (sqrtR ((sqrt_0 x),x)) . (n + 1) by XBOOLE_0:def 1;
y in (((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)))) \/ (sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n))) by A8, Th8;
then ( y in ((sqrtR ((sqrt_0 x),x)) . n) \/ (sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n))) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

per cases then ( y in (sqrtR ((sqrt_0 x),x)) . n or y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) or y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ) by XBOOLE_0:def 3;

suppose y in (sqrtR ((sqrt_0 x),x)) . n ; :: thesis: contradiction

hence contradiction by A7; :: thesis: verum

end;

suppose y in sqrt (x,((sqrtL ((sqrt_0 x),x)) . n),((sqrtL ((sqrt_0 x),x)) . n)) ; :: thesis: contradiction

then consider x1, y1 being Surreal such that
A9: ( x1 in (sqrtL ((sqrt_0 x),x)) . n & y1 in (sqrtL ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & y = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
x <= 0_No by A1;
then ( (sqrtL ((sqrt_0 x),x)) . n c= Union (sqrtL ((sqrt_0 x),x)) & Union (sqrtL ((sqrt_0 x),x)) = {} ) by ABCMIZ_1:1, Th18;
hence contradiction by A9; :: thesis: verum

end;

suppose y in sqrt (x,((sqrtR ((sqrt_0 x),x)) . n),((sqrtR ((sqrt_0 x),x)) . n)) ; :: thesis: contradiction

then ex x1, y1 being Surreal st
( x1 in (sqrtR ((sqrt_0 x),x)) . n & y1 in (sqrtR ((sqrt_0 x),x)) . n & not x1 + y1 == 0_No & y = (x +' (x1 * y1)) * ((x1 + y1) ") ) by Def2;
hence contradiction by A7; :: thesis: verum

end;

end;

end;

A10: for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A6);
A11: Union (sqrtR ((sqrt_0 x),x)) = {}

proof

assume Union (sqrtR ((sqrt_0 x),x)) <> {} ; :: thesis: contradiction
then consider a being object such that
A12: a in Union (sqrtR ((sqrt_0 x),x)) by XBOOLE_0:def 1;
consider n being object such that
A13: ( n in dom (sqrtR ((sqrt_0 x),x)) & a in (sqrtR ((sqrt_0 x),x)) . n ) by A12, CARD_5:2;
dom (sqrtR ((sqrt_0 x),x)) = NAT by Def5;
then reconsider n = n as Nat by A13;
(sqrtR ((sqrt_0 x),x)) . n = {} by A10;
hence contradiction by A13; :: thesis: verum

end;

x <= 0_No by A1;
then Union (sqrtL ((sqrt_0 x),x)) = {} by Th18;
hence sqrt x = 0_No by A11, Th15; :: thesis: verum