for e being set
for k being Nat st e in k -SD holds
e is Integer