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 Nat st
( l = k & l <> 0 & l divides n ) ;
hence ( 0 < k & k divides n ) ; :: thesis: verum

end;

thus ( 0 < k & k divides n implies k in NatDivisors n ) ; :: thesis: verum