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

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