let O be set ; :: thesis: for G being GroupWithOperators of O
for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of G st N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds
N1 "\/" N2 is normal StableSubgroup of H1
let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G
for N1, N2 being strict StableSubgroup of G st N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds
N1 "\/" N2 is normal StableSubgroup of H1
let H1 be StableSubgroup of G; :: thesis: for N1, N2 being strict StableSubgroup of G st N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 holds
N1 "\/" N2 is normal StableSubgroup of H1
let N1, N2 be strict StableSubgroup of G; :: thesis: ( N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 implies N1 "\/" N2 is normal StableSubgroup of H1 )
assume A1: ( N1 is normal StableSubgroup of H1 & N2 is normal StableSubgroup of H1 ) ; :: thesis: N1 "\/" N2 is normal StableSubgroup of H1
then reconsider N19 = N1, N29 = N2 as StableSubgroup of H1 ;
N1 "\/" N2 = N19 "\/" N29 by Th86;
hence N1 "\/" N2 is normal StableSubgroup of H1 by A1, Th32; :: thesis: verum