theorem Th4: :: CATALAN1:4

for n being Nat st n > 1 holds
(n -' 2) + 1 = n -' 1