Sum I = addint $$ I by Th16;
hence Sum I is Element of INT ; :: thesis: verum