L1,L2,L3:T List. L1 
L2 
L2 L3 L1 L3k,m:
, f:(k
m), g:(m
).
Thm* increasing(f;k)
increasing(g;m) increasing(g o f;k)| Rank | Theorem | Name |
| 2 | L1,L2,L3:T List. L1 L2 L2 L3 L1 L3 | [sublist_transitivity] |
| cites the following: | ||
| 1 | k,m:, f:(km), g:(m).
Thm* increasing(f;k) increasing(g;m) increasing(g o f;k) | [compose_increasing] |