let G be Group; :: thesis: for N1, N2 being strict normal Subgroup of G holds N1 "\/" N2 is normal Subgroup of G
let N1, N2 be strict normal Subgroup of G; :: thesis: N1 "\/" N2 is normal Subgroup of G
( ex N being strict normal Subgroup of G st the carrier of N = (carr N1) * (carr N2) & the carrier of (N1 "\/" N2) = N1 * N2 ) by Th53, GROUP_3:126;
hence N1 "\/" N2 is normal Subgroup of G by GROUP_2:59; :: thesis: verum