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

proof

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

end;

thus 33 + 1 is_a_product_of_two_different_primes :: thesis: 33 + 2 is_a_product_of_two_different_primes

proof

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

end;

thus 33 + 2 is_a_product_of_two_different_primes :: thesis: verum

proof

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

end;