{ k where k is Element of NAT : ( k <> 0 & k divides n ) } c= NAT

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { k where k is Element of NAT : ( k <> 0 & k divides n ) } or x in NAT )
assume x in { k where k is Element of NAT : ( k <> 0 & k divides n ) } ; :: thesis: x in NAT
then ex k being Element of NAT st
( k = x & k <> 0 & k divides n ) ;
hence x in NAT ; :: thesis: verum

end;

hence { k where k is Element of NAT : ( k <> 0 & k divides n ) } is Subset of NAT ; :: thesis: verum