for G being Group
for H being Subgroup of G holds
( ((1). G) /\ H = (1). G & H /\ ((1). G) = (1). G )