theorem :: NUMBER09:21

for n being Nat st n is a_product_of_two_primes holds
for a, b being Nat st a <> 1 & b <> 1 & n = a * b holds
( a is prime & b is prime ) by NUMBER07:59;