let O be set ; :: thesis: for G being GroupWithOperators of O
for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2
let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G holds H1 is StableSubgroup of H1 "\/" H2
let H1, H2 be StableSubgroup of G; :: thesis: H1 is StableSubgroup of H1 "\/" H2
( carr H1 c= (carr H1) \/ (carr H2) & (carr H1) \/ (carr H2) c= the carrier of (the_stable_subgroup_of ((carr H1) \/ (carr H2))) ) by Def26, XBOOLE_1:7;
hence H1 is StableSubgroup of H1 "\/" H2 by Lm20, XBOOLE_1:1; :: thesis: verum