let x be ExtReal; :: according to NUMBER15:def 2 :: thesis: ( x in SetPrimes implies x > 0 )
assume x in SetPrimes ; :: thesis: x > 0
then x is Prime by NEWTON:def 6;
hence x > 0 ; :: thesis: verum