theorem :: GROUP_24:48

for G being Group
for H, K being Subgroup of G st H is Subgroup of K holds
for N being Subgroup of G st N is normal Subgroup of K holds
( H,N are_complements_in K iff ( H * N = the carrier of K & H /\ N = (1). K ) )