let a, b be Nat; :: thesis: ( a divides b implies PrimeDivisors a c= PrimeDivisors b )
assume A1: a divides b ; :: thesis: PrimeDivisors a c= PrimeDivisors b
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors a or x in PrimeDivisors b )
assume x in PrimeDivisors a ; :: thesis: x in PrimeDivisors b
then consider q being Prime such that
A3: ( x = q & q divides a ) ;
q divides b by A1, A3, NAT_D:4;
hence x in PrimeDivisors b by A3; :: thesis: verum