:: deftheorem defines = GROUP_1A:def 16 :
for G being addGroup
for H1, H2 being strict Subgroup of G holds
( H1 = H2 iff for g being Element of G holds
( g in H1 iff g in H2 ) );