for k being natural Number holds k = { i where i is Nat : i < k }