theorem :: GROUP_1A:51

for G being addGroup holds - ({} the carrier of G) = {}