theorem :: NUMBER07:60

for n being Nat st n is_a_product_of_two_different_primes holds
for a, b being Nat st a <> 1 & b <> 1 & n = a * b holds
( a is prime & b is prime ) by Th59;