i,j:
. 0<i
j 
i
ij & jiji,j:
. iij & jija,b:. 0<ab 
0<a & 0<b| Rank | Theorem | Name |
| 5 | i,j:. 0<ij iij & jij | [pos_mul_arg_boundsNat2] |
| cites the following: | ||
| 2 | i,j:. iij & jij | [factors_bound] |
| 4 | a,b:. 0<ab 0<a & 0<b | [pos_mul_arg_boundsNat] |