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

for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

let H1, H2 be StableSubgroup of G; :: thesis: H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

reconsider Y = the carrier of (H19 "\/" H29) as Subset of G by GROUP_2:def 5;

A1: Y = the carrier of (gr (H19 * H29)) by GROUP_4:50;

H1 "\/" H2 = the_stable_subgroup_of Y by Lm31

.= the_stable_subgroup_of (H19 * H29) by A1, Lm31 ;

hence H1 "\/" H2 = the_stable_subgroup_of (H1 * H2) ; :: thesis: verum

for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

let G be GroupWithOperators of O; :: thesis: for H1, H2 being StableSubgroup of G holds H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

let H1, H2 be StableSubgroup of G; :: thesis: H1 "\/" H2 = the_stable_subgroup_of (H1 * H2)

reconsider H19 = H1, H29 = H2 as Subgroup of G by Def7;

reconsider Y = the carrier of (H19 "\/" H29) as Subset of G by GROUP_2:def 5;

A1: Y = the carrier of (gr (H19 * H29)) by GROUP_4:50;

H1 "\/" H2 = the_stable_subgroup_of Y by Lm31

.= the_stable_subgroup_of (H19 * H29) by A1, Lm31 ;

hence H1 "\/" H2 = the_stable_subgroup_of (H1 * H2) ; :: thesis: verum