let n be Nat; :: thesis: ( n is a_product_of_two_primes implies n >= 4 )
given p, q being Prime such that A1: n = p * q ; :: according to NUMBER09:def 3 :: thesis: n >= 4
A2: 4 = 2 * 2 ;
( 1 < p & 1 < q ) by INT_2:def 4;
then ( 1 + 1 <= p & 1 + 1 <= q ) by NAT_1:13;
hence n >= 4 by A1, A2, XREAL_1:66; :: thesis: verum