let O be set ; :: thesis: for G being GroupWithOperators of O
for N1, N2 being strict normal StableSubgroup of G holds N1 "\/" N2 is normal StableSubgroup of G
let G be GroupWithOperators of O; :: thesis: for N1, N2 being strict normal StableSubgroup of G holds N1 "\/" N2 is normal StableSubgroup of G
let N1, N2 be strict normal StableSubgroup of G; :: thesis: N1 "\/" N2 is normal StableSubgroup of G
( ex N being strict normal StableSubgroup of G st the carrier of N = (carr N1) * (carr N2) & the carrier of (N1 "\/" N2) = N1 * N2 ) by Th23, Th31;
hence N1 "\/" N2 is normal StableSubgroup of G by Lm4; :: thesis: verum