theorem Th63: :: NUMBER07:63

for a, n being Nat st a <> 1 & a <> n & not a is prime & a divides n holds
not n is_a_product_of_two_different_primes by GR_CY_3:1;