let i be Integer; :: thesis: PrimeDivisors i c= SetPrimes
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors i or x in SetPrimes )
assume x in PrimeDivisors i ; :: thesis: x in SetPrimes
then ex k being Prime st
( x = k & k divides i ) ;
hence x in SetPrimes by NEWTON:def 6; :: thesis: verum