take 0 ; :: thesis: 0 is integer
thus 0 in INT by Def1; :: according to INT_1:def 2 :: thesis: verum