let O be set ; :: thesis: for G being GroupWithOperators of O

for H1 being StableSubgroup of G

for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let H1 be StableSubgroup of G; :: thesis: for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let H2, H3 be strict StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H2 implies H1 "\/" H3 is StableSubgroup of H2 "\/" H3 )

assume H1 is StableSubgroup of H2 ; :: thesis: H1 "\/" H3 is StableSubgroup of H2 "\/" H3

then H1 is Subgroup of H2 by Def7;

then carr H1 c= carr H2 by GROUP_2:def 5;

hence H1 "\/" H3 is StableSubgroup of H2 "\/" H3 by Th26, XBOOLE_1:9; :: thesis: verum

for H1 being StableSubgroup of G

for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let G be GroupWithOperators of O; :: thesis: for H1 being StableSubgroup of G

for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let H1 be StableSubgroup of G; :: thesis: for H2, H3 being strict StableSubgroup of G st H1 is StableSubgroup of H2 holds

H1 "\/" H3 is StableSubgroup of H2 "\/" H3

let H2, H3 be strict StableSubgroup of G; :: thesis: ( H1 is StableSubgroup of H2 implies H1 "\/" H3 is StableSubgroup of H2 "\/" H3 )

assume H1 is StableSubgroup of H2 ; :: thesis: H1 "\/" H3 is StableSubgroup of H2 "\/" H3

then H1 is Subgroup of H2 by Def7;

then carr H1 c= carr H2 by GROUP_2:def 5;

hence H1 "\/" H3 is StableSubgroup of H2 "\/" H3 by Th26, XBOOLE_1:9; :: thesis: verum