let n be Nat; :: thesis: ( n = born (uInt . n) & n = born (uInt . (- n)) )
A1: uInt . n in Day n by Th1;
for O being Ordinal st uInt . n in Day O holds
n c= O

proof

let O be Ordinal; :: thesis: ( uInt . n in Day O implies n c= O )
assume that
A2: uInt . n in Day O and
A3: not n c= O ; :: thesis: contradiction
A4: O in Segm n by A3, ORDINAL1:16;
reconsider O = O as Nat by A3;
( uInt . n <= uInt . O & uInt . O < uInt . n ) by A2, Th2, A4, NAT_1:44, Th3;
hence contradiction ; :: thesis: verum

end;

hence n = born (uInt . n) by A1, SURREAL0:def 18; :: thesis: n = born (uInt . (- n))
A5: uInt . (- n) in Day n by Th1;
for O being Ordinal st uInt . (- n) in Day O holds
n c= O

proof

let O be Ordinal; :: thesis: ( uInt . (- n) in Day O implies n c= O )
assume that
A6: uInt . (- n) in Day O and
A7: not n c= O ; :: thesis: contradiction
A8: O in Segm n by A7, ORDINAL1:16;
reconsider O = O as Nat by A7;
A9: - n < - O by XREAL_1:24, A8, NAT_1:44;
( uInt . (- n) <= uInt . (- O) & uInt . (- O) < uInt . (- n) ) by A6, Th2, A9, Th3;
hence contradiction ; :: thesis: verum

end;

hence n = born (uInt . (- n)) by A5, SURREAL0:def 18; :: thesis: verum