x:{2...}. 
p:{2...}. p
x & prime(p) & p | xx:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = p
c| Rank | Theorem | Name |
| 14 | x:{2...}. p:{2...}. px & prime(p) & p | x | [prime_or_smaller_prime_factor] |
| cites the following: | ||
| 13 | x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc | [prime_or_smaller_prime_factor2] |