let n, k be Nat; :: 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 12;
hence k in NatDivisors n by A1; :: thesis: verum