let k, l be Nat; :: thesis: ( k divides l iff ex t being Nat st l = k * t )

hence k divides l ; :: thesis: verum

hereby :: thesis: ( ex t being Nat st l = k * t implies k divides l )

assume
ex t being Nat st l = k * t
; :: thesis: k divides lassume A1:
k divides l
; :: thesis: ex t being Nat st l = k * t

thus ex t being Nat st l = k * t :: thesis: verum

end;thus ex t being Nat st l = k * t :: thesis: verum

hence k divides l ; :: thesis: verum