theorem :: CATALAN1:17

for n being Nat holds Catalan n >= 0 ;