reconsider e = 0 as Element of INT.Group by INT_1:def 2;
for h being Element of INT.Group holds
( h * e = h & e * h = h ) ;
hence 1_ INT.Group = 0 by GROUP_1:4; :: thesis: verum