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
consider N being strict normal Subgroup of G such that
A1: the carrier of N = (carr N1) * (carr N2) by GROUP_3:149;
( the carrier of (N1 "\/" N2) = N1 * N2 & N1 * N2 = (carr N1) * (carr N2) ) by Th71;
hence N1 "\/" N2 is normal Subgroup of G by A1, GROUP_2:68; :: thesis: verum