for G being strict Group
for H being Subgroup of G holds
( ( for a, b being Element of G st b is Element of H holds
b |^ a in H ) iff H is normal ) by Lm1, Lm2;