theorem :: STIRL2_1:33

for k, n being Nat holds
( ( ( 1 <= k & k <= n ) or k = n ) iff n block k > 0 )