k:
, f:(k
k). increasing(f;k) 
(i:k. f(i) = i)k:, f:(k
). increasing(f;k) (x,y:k. x<y f(x)<f(y))| Theorem | Name |
| k:, f:(kk). increasing(f;k) (i:k. f(i) = i) | [increasing_is_id] |
| cites the following: | |
| k:, f:(k). increasing(f;k) (x,y:k. x<y f(x)<f(y)) | [increasing_implies] |