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