theorem Th20: :: GROUP_1A:20

for G being non empty add-unital addMagma holds 0_ G is_a_unity_wrt the addF of G