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

k is Element of NAT by ORDINAL1:def 12;

hence k in NatDivisors n by A1; :: thesis: verum

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

assume A1:
( 0 < k & k divides n )
; :: thesis: k in NatDivisors nassume
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;then ex l being Element of NAT st

( l = k & l <> 0 & l divides n ) ;

hence ( 0 < k & k divides n ) ; :: thesis: verum

k is Element of NAT by ORDINAL1:def 12;

hence k in NatDivisors n by A1; :: thesis: verum