let n, k be natural number ; :: thesis: ( k in NatDivisors n iff ( 0 < k & k divides n ) )

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

assume k in NatDivisors n ; :: thesis: ( 0 < k & k divides n )
then ex l being Element of NAT st
( l = k & l <> 0 & l divides n ) ;
hence ( 0 < k & k divides n ) ; :: thesis: verum

end;

assume A1: ( 0 < k & k divides n ) ; :: thesis: k in NatDivisors n
k is Element of NAT by ORDINAL1:def 13;
hence k in NatDivisors n by A1; :: thesis: verum