let n be Nat; :: thesis: ( n is_a_product_of_two_different_primes implies n >= 6 )
given p, q being Prime such that A1: p <> q and
A2: n = p * q ; :: according to NUMBER07:def 5 :: thesis: n >= 6
A3: 6 = 2 * 3 ;
( ( 2 <= p & 3 <= q ) or ( 3 <= p & 2 <= q ) ) by A1, Th40;
hence n >= 6 by A2, A3, XREAL_1:66; :: thesis: verum