let n be Nat; :: thesis: ( uInt . n in Day n & uInt . (- n) in Day n )
defpred S₁[ Nat] means ( uInt . $1 in Day $1 & uInt . (- $1) in Day $1 );
A1: uInt . 0 = 0_No by Def1;
born 0_No = {} by SURREAL0:37;
then A2: S₁[ 0 ] by A1, SURREAL0:def 18;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
A5: {(uInt . n)} << {} ;
A6: ( n in succ (Segm n) & succ (Segm n) = Segm (n + 1) ) by ORDINAL1:6, NAT_1:38;
A7: {} << {(uInt . (- n))} ;
A8: for o being object st o in {(uInt . (- n))} \/ {} holds
ex O being Ordinal st
( O in n + 1 & o in Day O )

proof

let o be object ; :: thesis: ( o in {(uInt . (- n))} \/ {} implies ex O being Ordinal st
( O in n + 1 & o in Day O ) )
assume o in {(uInt . (- n))} \/ {} ; :: thesis: ex O being Ordinal st
( O in n + 1 & o in Day O )
then o = uInt . (- n) by TARSKI:def 1;
hence ex O being Ordinal st
( O in n + 1 & o in Day O ) by A6, A4; :: thesis: verum

end;

for o being object st o in {(uInt . n)} \/ {} holds
ex O being Ordinal st
( O in n + 1 & o in Day O )

proof

let o be object ; :: thesis: ( o in {(uInt . n)} \/ {} implies ex O being Ordinal st
( O in n + 1 & o in Day O ) )
assume o in {(uInt . n)} \/ {} ; :: thesis: ex O being Ordinal st
( O in n + 1 & o in Day O )
then o = uInt . n by TARSKI:def 1;
hence ex O being Ordinal st
( O in n + 1 & o in Day O ) by A6, A4; :: thesis: verum

end;

then ( [{(uInt . n)},{}] in Day (n + 1) & [{},{(uInt . (- n))}] in Day (n + 1) ) by A8, A5, A7, SURREAL0:46;
hence S₁[n + 1] by Def1; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence ( uInt . n in Day n & uInt . (- n) in Day n ) ; :: thesis: verum