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