theorem :: GROUP_24:51

for G being Group
for K being Subgroup of G
for H being Subgroup of K
for N being normal Subgroup of G st N is Subgroup of K holds
( H,N are_complements_in K iff H,(K,N) `*` are_complements_in K ) by Th46;