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 H1' = H1, H2' = H2 as Subgroup of G by Def7;
reconsider Y = the carrier of (H1' "\/" H2') as Subset of G by GROUP_2:def 5;
A1: Y = the carrier of (gr (H1' * H2')) by GROUP_4:68;
H1 "\/" H2 = the_stable_subgroup_of Y by Lm32
.= the_stable_subgroup_of (H1' * H2') by A1, Lm32 ;
hence H1 "\/" H2 = the_stable_subgroup_of (H1 * H2) ; :: thesis: verum