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