let n, k be natural number ; :: thesis: ( k in NatDivisors n iff ( 0 < k & k divides n ) )
A1: k is Element of NAT by ORDINAL1:def 13;

hereby :: thesis: ( 0 < k & k divides n implies k in NatDivisors n )

assume k in NatDivisors n ; :: thesis: ( 0 < k & k divides n )
then consider l being Element of NAT such that
A2: ( l = k & l <> 0 & l divides n ) ;
thus ( 0 < k & k divides n ) by A2; :: thesis: verum

end;

assume ( 0 < k & k divides n ) ; :: thesis: k in NatDivisors n
hence k in NatDivisors n by A1; :: thesis: verum