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