let p be Prime; :: thesis: PrimeDivisors p = {p}
thus PrimeDivisors p c= {p} :: according to XBOOLE_0:def 10 :: thesis: {p} c= PrimeDivisors p

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors p or x in {p} )
assume x in PrimeDivisors p ; :: thesis: x in {p}
then consider k being Prime such that
S1: ( k = x & k divides p ) ;
( k = p or k = 1 ) by S1, INT_2:def 4;
hence x in {p} by S1, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {p} or x in PrimeDivisors p )
assume x in {p} ; :: thesis: x in PrimeDivisors p
then x = p by TARSKI:def 1;
hence x in PrimeDivisors p ; :: thesis: verum