theorem :: NUMBER07:76
( 36 = ((2 * 2) * 3) * 3 & 36 has_exactly_two_different_prime_divisors )