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

proof

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

end;

thus 141 + 1 is_a_product_of_two_different_primes :: thesis: 141 + 2 is_a_product_of_two_different_primes

proof

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

end;

thus 141 + 2 is_a_product_of_two_different_primes :: thesis: verum

proof

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

end;