set n = 201;
thus 201 is_a_product_of_two_different_primes :: according to NUMBER07:def 6 :: thesis: ( 201 + 1 is_a_product_of_two_different_primes & 201 + 2 is_a_product_of_two_different_primes )
proof
take P3 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P3 <> q & 201 = P3 * q )
take P67 ; :: thesis: ( P3 <> P67 & 201 = P3 * P67 )
thus ( P3 <> P67 & 201 = P3 * P67 ) ; :: thesis: verum
end;
thus 201 + 1 is_a_product_of_two_different_primes :: thesis: 201 + 2 is_a_product_of_two_different_primes
proof
take P2 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P2 <> q & 201 + 1 = P2 * q )
take P101 ; :: thesis: ( P2 <> P101 & 201 + 1 = P2 * P101 )
thus ( P2 <> P101 & 201 + 1 = P2 * P101 ) ; :: thesis: verum
end;
thus 201 + 2 is_a_product_of_two_different_primes :: thesis: verum
proof
take P7 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P7 <> q & 201 + 2 = P7 * q )
take P29 ; :: thesis: ( P7 <> P29 & 201 + 2 = P7 * P29 )
thus ( P7 <> P29 & 201 + 2 = P7 * P29 ) ; :: thesis: verum
end;