theorem Th82: :: GROUP_24:77

for g being Element of (INT.Group 2) st g = 1 holds
g * g = 1_ (INT.Group 2)