k,m:
, f:(k
m). increasing(f;k) 
Inj(k; m; f)k:, f:(k
). increasing(f;k) (x,y:k. x<y f(x)<f(y))| Theorem | Name |
| k,m:, f:(km). increasing(f;k) Inj(k; m; f) | [increasing_inj] |
| cites the following: | |
| k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) | [increasing_implies] |