let G be Group; :: thesis: 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,N are_complements_in K iff H,(K,N) `*` are_complements_in K )
let H, K be Subgroup of G; :: thesis: ( H is Subgroup of K implies 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 ) )
assume A1: H is Subgroup of K ; :: thesis: 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 )
let N be normal Subgroup of G; :: thesis: ( N is Subgroup of K implies ( H,N are_complements_in K iff H,(K,N) `*` are_complements_in K ) )
assume A2: N is Subgroup of K ; :: thesis: ( H,N are_complements_in K iff H,(K,N) `*` are_complements_in K )
then A3: N is normal Subgroup of K by GROUP_6:8;

hereby :: thesis: ( H,(K,N) `*` are_complements_in K implies H,N are_complements_in K )

assume H,N are_complements_in K ; :: thesis: H,(K,N) `*` are_complements_in K
then ( N * H = the carrier of K & H /\ N = (1). K ) by A1, A3, Th43;
hence H,(K,N) `*` are_complements_in K by A1, A2, Th45; :: thesis: verum

end;

assume H,(K,N) `*` are_complements_in K ; :: thesis: H,N are_complements_in K
then ( N * H = the carrier of K & H /\ N = (1). K ) by A1, A2, Th45;
hence H,N are_complements_in K by A1, A3, Th43; :: thesis: verum