let o be object ; :: thesis: for x being Surreal st x <= 0_No holds
Union (sqrtL ((sqrt_0 x),o)) = {}
let x be Surreal; :: thesis: ( x <= 0_No implies Union (sqrtL ((sqrt_0 x),o)) = {} )
assume A1: x <= 0_No ; :: thesis: Union (sqrtL ((sqrt_0 x),o)) = {}
defpred S₁[ Nat] means (sqrtL ((sqrt_0 x),o)) . $1 = {} ;
A2: S₁[ 0 ]

proof

assume (sqrtL ((sqrt_0 x),o)) . 0 <> {} ; :: thesis: contradiction
then consider a being object such that
A3: a in (sqrtL ((sqrt_0 x),o)) . 0 by XBOOLE_0:def 1;
a in L_ (sqrt_0 x) by A3, Th6;
then consider l being Surreal such that
A4: ( a = sqrt l & l in L_ (NonNegativePart x) ) by Def9;
A5: ( l in L_ x & 0_No <= l ) by A4, Th2;
( L_ x << {x} & x in {x} ) by TARSKI:def 1, SURREALO:11;
hence contradiction by A5, A1, SURREALO:4; :: 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 (sqrtL ((sqrt_0 x),o)) . (n + 1) <> {} ; :: thesis: contradiction
then consider y being object such that
A8: y in (sqrtL ((sqrt_0 x),o)) . (n + 1) by XBOOLE_0:def 1;
y in ((sqrtL ((sqrt_0 x),o)) . n) \/ (sqrt (o,((sqrtL ((sqrt_0 x),o)) . n),((sqrtR ((sqrt_0 x),o)) . n))) by A8, Th8;

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

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

hence contradiction by A7; :: thesis: verum

end;

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

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

end;

end;

end;

A9: for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A6);
assume Union (sqrtL ((sqrt_0 x),o)) <> {} ; :: thesis: contradiction
then consider a being object such that
A10: a in Union (sqrtL ((sqrt_0 x),o)) by XBOOLE_0:def 1;
consider n being object such that
A11: ( n in dom (sqrtL ((sqrt_0 x),o)) & a in (sqrtL ((sqrt_0 x),o)) . n ) by A10, CARD_5:2;
dom (sqrtL ((sqrt_0 x),o)) = NAT by Def4;
then reconsider n = n as Nat by A11;
(sqrtL ((sqrt_0 x),o)) . n = {} by A9;
hence contradiction by A11; :: thesis: verum