theorem :: STIRL2_1:22

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