for j, k being Nat st 0 < k & k <= j & k mod j = 0 holds
k = j