let n be Nat; :: thesis: PrimeDivisors n c= NatDivisors n
PrimeDivisors n c= NatDivisors n

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in PrimeDivisors n or x in NatDivisors n )
assume x in PrimeDivisors n ; :: thesis: x in NatDivisors n
then consider k being Prime such that
A1: ( x = k & k divides n ) ;
k in { l where l is Nat : ( l <> 0 & l divides n ) } by A1;
hence x in NatDivisors n by A1, MOEBIUS1:def 4; :: thesis: verum

end;

hence PrimeDivisors n c= NatDivisors n ; :: thesis: verum