theorem Th8: :: RADIX_3:8

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