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