let n be non zero Nat; :: thesis: { k where k is Nat : k divides n } is finite
set A = { k where k is Nat : k divides n } ;
{ k where k is Nat : k divides n } c= NatDivisors n

proof

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

end;

hence { k where k is Nat : k divides n } is finite ; :: thesis: verum