theorem Th16: :: CATALAN1:16

for n being Nat holds Catalan n <= Catalan (n + 1)