theorem Th4: :: FIB_NUM3:4

for k being non zero Nat holds (k -' 1) + 2 = (k + 2) -' 1