theorem Th23: :: STIRL2_1:23

for k, n being Nat holds
not ( ( n = 0 implies k = 0 ) & ( k = 0 implies n = 0 ) & n >= k & ( for f being Function of (Segm n),(Segm k) holds
( not f is onto or not f is "increasing ) ) )