let O be set ; :: thesis:
let G be GroupWithOperators of O; :: thesis:
let H1, H2 be StableSubgroup of G; :: thesis:
assume H1 * H2 = H2 * H1 ; :: thesis:
then consider H being strict StableSubgroup of G such that
A1: the carrier of H = (carr H1) * (carr H2) by Th17;

set A = (carr H1) \/ (carr H2);
let a be Element of G; :: thesis:
set X = { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;
assume a in H ; :: thesis:
then a in (carr H1) * (carr H2) by A1, STRUCT_0:def 5;
then consider b, c being Element of G such that
A2: a = b * c and
A3: b in carr H1 and
A4: c in carr H2 ;

let Y be set ; :: thesis:
assume Y in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ; :: thesis:
then consider B being Subset of G such that
A6: Y = B and
A7: ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) ;
consider H9 being strict StableSubgroup of G such that
A8: B = the carrier of H9 and
A9: (carr H1) \/ (carr H2) c= carr H9 by A7;
c in (carr H1) \/ (carr H2) by A4, XBOOLE_0:def 3;
then A10: c in H9 by A9, STRUCT_0:def 5;
A11: H9 is Subgroup of G by Def7;
b in (carr H1) \/ (carr H2) by A3, XBOOLE_0:def 3;
then b in H9 by A9, STRUCT_0:def 5;
then b * c in H9 by A11, A10, GROUP_2:50;
hence a in Y by A2, A6, A8, STRUCT_0:def 5; :: thesis:

end;

carr ((Omega). G) in { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } ;
then a in meet { B where B is Subset of G : ex H being strict StableSubgroup of G st
( B = the carrier of H & (carr H1) \/ (carr H2) c= carr H ) } by A5, SETFAM_1:def 1;
then a in the carrier of (the_stable_subgroup_of ((carr H1) \/ (carr H2))) by Th27;
hence a in H1 "\/" H2 by STRUCT_0:def 5; :: thesis:

end;

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A13: x in (carr H1) \/ (carr H2) ; :: thesis:
then reconsider a = x as Element of G ;

end;

end;

hence x in (carr H1) * (carr H2) ; :: thesis:

end;