let n be Nat; for i being Integer st - n < i & i < n holds
( uInt . (- n) < uInt . i & uInt . i < uInt . n )
let i be Integer; ( - n < i & i < n implies ( uInt . (- n) < uInt . i & uInt . i < uInt . n ) )
assume A1:
( - n < i & i < n )
; ( uInt . (- n) < uInt . i & uInt . i < uInt . n )
i in INT
by INT_1:def 2;
then consider k being Nat such that
A2:
( i = k or i = - k )
by INT_1:def 1;
Segm k c= Segm n
by A2, A1, XREAL_1:24, NAT_1:39;
then A3:
Day k c= Day n
by SURREAL0:35;
A4:
( born_eq (uInt . n) = n & n = born_eq (uInt . (- n)) )
by Th5;
born_eq (uInt . i) = k
by A2, Th5;
then A5:
( not uInt . n == uInt . i & not uInt . i == uInt . (- n) )
by A4, SURREALO:50, A2, A1;
born (uInt . i) = k
by A2, Th4;
then
uInt . i in Day k
by SURREAL0:def 18;
hence
( uInt . (- n) < uInt . i & uInt . i < uInt . n )
by Th2, A5, A3; verum