for G being addGroup
for H2, H1 being Subgroup of G holds
( H1 is Subgroup of H2 iff addMagma(# the carrier of (H1 /\ H2), the addF of (H1 /\ H2) #) = addMagma(# the carrier of H1, the addF of H1 #) ) by Lm3;