thus PrimeDivisors 0 c= SetPrimes :: according to XBOOLE_0:def 10 :: thesis: SetPrimes c= PrimeDivisors 0

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors 0 or x in SetPrimes )
assume x in PrimeDivisors 0 ; :: thesis: x in SetPrimes
then consider k being Prime such that
A1: ( x = k & k divides 0 ) ;
thus x in SetPrimes by A1, NEWTON:def 6; :: thesis: verum

end;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in SetPrimes or p in PrimeDivisors 0 )
assume p in SetPrimes ; :: thesis: p in PrimeDivisors 0
then reconsider pp = p as Prime by NEWTON:def 6;
pp divides 0 by NAT_D:6;
hence p in PrimeDivisors 0 ; :: thesis: verum