let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng uInt or y in Day NAT )
assume y in rng uInt ; :: thesis: y in Day NAT
then consider x being object such that
A1: ( x in dom uInt & uInt . x = y ) by FUNCT_1:def 3;
reconsider x = x as Integer by A1;
consider k being Nat such that
A2: ( x = k or x = - k ) by A1, INT_1:def 1;
k c= NAT ;
then A3: Day k c= Day NAT by SURREAL0:35;
y in Day k by A1, A2, Th1;
hence y in Day NAT by A3; :: thesis: verum