x:{2...}. 
p:{2...}, c:{1...}. p
x & prime(p) & x = p
cx:{2...}. 
prime(x) 
(i,j:{2..x
}. x = ij & prime(i))| Rank | Theorem | Name |
| 13 | x:{2...}. p:{2...}, c:{1...}. px & prime(p) & x = pc | [prime_or_smaller_prime_factor2] |
| cites the following: | ||
| 12 | x:{2...}. prime(x) (i,j:{2..x}. x = ij & prime(i)) | [composite_with_prime_factor] |