let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G
for H3 being strict StableSubgroup of G st H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 holds
H1 "\/" H2 is StableSubgroup of H3
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G
for H3 being strict StableSubgroup of G st H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 holds
H1 "\/" H2 is StableSubgroup of H3
let H1, H2 be StableSubgroup of G; :: thesis: for H3 being strict StableSubgroup of G st H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 holds
H1 "\/" H2 is StableSubgroup of H3
let H3 be strict StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H3 & H2 is StableSubgroup of H3 implies H1 "\/" H2 is StableSubgroup of H3 )
assume that
A1: H1 is StableSubgroup of H3 and
A2: H2 is StableSubgroup of H3 ; :: thesis: H1 "\/" H2 is StableSubgroup of H3
H2 is Subgroup of H3 by A2, Def7;
then A3: carr H2 c= carr H3 by GROUP_2:def 5;
H1 is Subgroup of H3 by A1, Def7;
then carr H1 c= carr H3 by GROUP_2:def 5;
then the_stable_subgroup_of ((carr H1) \/ (carr H2)) is StableSubgroup of the_stable_subgroup_of (carr H3) by A3, Th26, XBOOLE_1:8;
hence H1 "\/" H2 is StableSubgroup of H3 by Th25; :: thesis: verum