let n, k be Nat; :: thesis: ( k divides n implies PrimeDivisors k c= PrimeDivisors n )
assume A1: k divides n ; :: thesis: PrimeDivisors k c= PrimeDivisors n
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors k or x in PrimeDivisors n )
assume x in PrimeDivisors k ; :: thesis: x in PrimeDivisors n
then x in { p where p is Prime : p divides k } by NUMBER12:def 3;
then consider p being Prime such that
A2: ( x = p & p divides k ) ;
p divides n by A1, A2, INT_2:9;
then p in { p where p is Prime : p divides n } ;
hence x in PrimeDivisors n by A2, NUMBER12:def 3; :: thesis: verum