thus A1: 33 = 3 * 11 ; :: thesis: 33 has_exactly_two_different_prime_divisors
take P3 ; :: according to NUMBER07:def 4 :: thesis: ex q being Prime st
( P3 <> q & P3 divides 33 & q divides 33 & ( for r being Prime st r <> P3 & r <> q holds
not r divides 33 ) )
take P11 ; :: thesis: ( P3 <> P11 & P3 divides 33 & P11 divides 33 & ( for r being Prime st r <> P3 & r <> P11 holds
not r divides 33 ) )
thus P3 <> P11 ; :: thesis: ( P3 divides 33 & P11 divides 33 & ( for r being Prime st r <> P3 & r <> P11 holds
not r divides 33 ) )
thus P3 divides 33 by A1; :: thesis: ( P11 divides 33 & ( for r being Prime st r <> P3 & r <> P11 holds
not r divides 33 ) )
thus P11 divides 33 by A1; :: thesis: for r being Prime st r <> P3 & r <> P11 holds
not r divides 33
let r be Prime; :: thesis: ( r <> P3 & r <> P11 implies not r divides 33 )
assume A2: ( r <> P3 & r <> P11 ) ; :: thesis: not r divides 33
assume r divides 33 ; :: thesis: contradiction
then ( r divides 3 or r divides 11 ) by A1, INT_5:7;
hence contradiction by A2, XPRIMES0:1, XPRIMES1:3, XPRIMES1:11; :: thesis: verum