theorem :: GROUP_1A:296

for G being addGroup
for A being Subset of G holds A in con_class A ;