theorem Th1: :: SURREALN:1

for n being Nat holds
( uInt . n in Day n & uInt . (- n) in Day n )