theorem Th45: :: GROUP_24:49

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