set n = 85;
thus 85 is_a_product_of_two_different_primes :: according to NUMBER07:def 6 :: thesis: ( 85 + 1 is_a_product_of_two_different_primes & 85 + 2 is_a_product_of_two_different_primes )

proof

take P5 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P5 <> q & 85 = P5 * q )
take P17 ; :: thesis: ( P5 <> P17 & 85 = P5 * P17 )
thus ( P5 <> P17 & 85 = P5 * P17 ) ; :: thesis: verum

end;

thus 85 + 1 is_a_product_of_two_different_primes :: thesis: 85 + 2 is_a_product_of_two_different_primes

proof

take P2 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P2 <> q & 85 + 1 = P2 * q )
take P43 ; :: thesis: ( P2 <> P43 & 85 + 1 = P2 * P43 )
thus ( P2 <> P43 & 85 + 1 = P2 * P43 ) ; :: thesis: verum

end;

thus 85 + 2 is_a_product_of_two_different_primes :: thesis: verum

proof

take P3 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P3 <> q & 85 + 2 = P3 * q )
take P29 ; :: thesis: ( P3 <> P29 & 85 + 2 = P3 * P29 )
thus ( P3 <> P29 & 85 + 2 = P3 * P29 ) ; :: thesis: verum

end;