set n = 93;
thus 93 is_a_product_of_two_different_primes :: according to NUMBER07:def 6 :: thesis: ( 93 + 1 is_a_product_of_two_different_primes & 93 + 2 is_a_product_of_two_different_primes )
proof
take P3 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P3 <> q & 93 = P3 * q )
take P31 ; :: thesis: ( P3 <> P31 & 93 = P3 * P31 )
thus ( P3 <> P31 & 93 = P3 * P31 ) ; :: thesis: verum
end;
thus 93 + 1 is_a_product_of_two_different_primes :: thesis: 93 + 2 is_a_product_of_two_different_primes
proof
take P2 ; :: according to NUMBER07:def 5 :: thesis: ex q being Prime st
( P2 <> q & 93 + 1 = P2 * q )
take P47 ; :: thesis: ( P2 <> P47 & 93 + 1 = P2 * P47 )
thus ( P2 <> P47 & 93 + 1 = P2 * P47 ) ; :: thesis: verum
end;
thus 93 + 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 & 93 + 2 = P5 * q )
take P19 ; :: thesis: ( P5 <> P19 & 93 + 2 = P5 * P19 )
thus ( P5 <> P19 & 93 + 2 = P5 * P19 ) ; :: thesis: verum
end;