let n be Nat; :: thesis: ( L_ (uInt . (- n)) = {} & {} = R_ (uInt . n) )
A1: uInt . 0 = 0_No by Def1;
thus L_ (uInt . (- n)) = {} :: thesis: {} = R_ (uInt . n)

proof

assume A2: L_ (uInt . (- n)) <> {} ; :: thesis: contradiction
then n <> 0 by A1;
then reconsider N = n - 1 as Nat by NAT_1:20;
uInt . (- (N + 1)) = [{},{(uInt . (- N))}] by Def1;
hence contradiction by A2; :: thesis: verum

end;

assume A3: R_ (uInt . n) <> {} ; :: thesis: contradiction
then n <> 0 by A1;
then reconsider N = n - 1 as Nat by NAT_1:20;
uInt . (N + 1) = [{(uInt . N)},{}] by Def1;
hence contradiction by A3; :: thesis: verum