let n be Nat; :: thesis: ( born_eq (uInt . n) = n & born_eq (uInt . (- n)) = n )
A1: born (uInt . n) = n by Th4;
for y being Surreal st y == uInt . n holds
born (uInt . n) c= born y

proof

let y be Surreal; :: thesis: ( y == uInt . n implies born (uInt . n) c= born y )
assume A2: y == uInt . n ; :: thesis: born (uInt . n) c= born y
assume not born (uInt . n) c= born y ; :: thesis: contradiction
then A3: not n c= born y by Th4;
then reconsider O = born y as Nat ;
( y in Day O & Day O c= Day n ) by SURREAL0:35, SURREAL0:def 18, A3;
then y <= uInt . O by Th2;
then A4: uInt . n <= uInt . O by A2, SURREALO:4;
O in Segm n by A3, ORDINAL1:16;
hence contradiction by A4, Th3, NAT_1:44; :: thesis: verum

end;

hence born_eq (uInt . n) = n by A1, SURREALO:def 5; :: thesis: born_eq (uInt . (- n)) = n
A5: born (uInt . (- n)) = n by Th4;
for y being Surreal st y == uInt . (- n) holds
born (uInt . (- n)) c= born y

proof

let y be Surreal; :: thesis: ( y == uInt . (- n) implies born (uInt . (- n)) c= born y )
assume A6: y == uInt . (- n) ; :: thesis: born (uInt . (- n)) c= born y
assume not born (uInt . (- n)) c= born y ; :: thesis: contradiction
then A7: not n c= born y by Th4;
then reconsider O = born y as Nat ;
( y in Day O & Day O c= Day n ) by SURREAL0:35, SURREAL0:def 18, A7;
then A8: uInt . (- O) <= y by Th2;
O in Segm n by A7, ORDINAL1:16;
then - n < - O by NAT_1:44, XREAL_1:24;
hence contradiction by A8, A6, SURREALO:4, Th3; :: thesis: verum

end;

hence born_eq (uInt . (- n)) = n by A5, SURREALO:def 5; :: thesis: verum