theorem Th63: :: GROUP_1A:109

for G being addGroup
for H being Subgroup of G holds (0). H = (0). G