:: deftheorem Def12 defines con_class GROUP_1A:def 40 :
for G being addGroup
for H being Subgroup of G
for b₃ being Subset of (Subgroups G) holds
( b₃ = con_class H iff for x being object holds
( x in b₃ iff ex H1 being strict Subgroup of G st
( x = H1 & H,H1 are_conjugated ) ) );