for G being addGroup
for H being Subgroup of G holds
( ((0). G) /\ H = (0). G & H /\ ((0). G) = (0). G )