theorem Th5: :: CATALAN2:5

for m, n being Nat st n >= m holds
(n --> 0) ^ (m --> 1) is dominated_by_0