:: deftheorem defines block STIRL2_1:def 2 :
for n, k being Nat holds n block k = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;