let G be Group; :: thesis: for H1, H2 being Subgroup of G holds
( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
let H1, H2 be Subgroup of G; :: thesis: ( ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) & ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) ) )
thus ( (carr H1) * (carr H2) = (carr H2) * (carr H1) implies ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) ) :: thesis: ( ex H being Subgroup of G st the carrier of H = (carr H1) * (carr H2) implies (carr H1) * (carr H2) = (carr H2) * (carr H1) )

proof

assume A1: (carr H1) * (carr H2) = (carr H2) * (carr H1) ; :: thesis: ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2)
A2: (carr H1) * (carr H2) <> {} by Th13;

A3: now

let g1, g2 be Element of G; :: thesis: ( g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) implies g1 * g2 in (carr H1) * (carr H2) )
assume that
A4: g1 in (carr H1) * (carr H2) and
A5: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)
consider a1, b1 being Element of G such that
A6: ( g1 = a1 * b1 & a1 in carr H1 & b1 in carr H2 ) by A4;
consider a2, b2 being Element of G such that
A7: ( g2 = a2 * b2 & a2 in carr H1 & b2 in carr H2 ) by A5;
A8: g1 * g2 = ((a1 * b1) * a2) * b2 by A6, A7, GROUP_1:def 4
.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 4 ;
b1 * a2 in (carr H1) * (carr H2) by A1, A6, A7;
then consider a, b being Element of G such that
A9: ( b1 * a2 = a * b & a in carr H1 & b in carr H2 ) ;
A10: g1 * g2 = ((a1 * a) * b) * b2 by A8, A9, GROUP_1:def 4
.= (a1 * a) * (b * b2) by GROUP_1:def 4 ;
( a1 * a in carr H1 & b * b2 in carr H2 ) by A6, A7, A9, Th89;
hence g1 * g2 in (carr H1) * (carr H2) by A10; :: thesis: verum

end;

now

let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )
assume A11: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A12: ( g = a * b & a in carr H1 & b in carr H2 ) ;
consider b1, a1 being Element of G such that
A13: ( a * b = b1 * a1 & b1 in carr H2 & a1 in carr H1 ) by A1, A11, A12;
A14: g " = (a1 " ) * (b1 " ) by A12, A13, GROUP_1:25;
( a1 " in carr H1 & b1 " in carr H2 ) by A13, Th90;
hence g " in (carr H1) * (carr H2) by A14; :: thesis: verum

end;

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A2, A3, Th61; :: thesis: verum

end;

given H being Subgroup of G such that A15: the carrier of H = (carr H1) * (carr H2) ; :: thesis: (carr H1) * (carr H2) = (carr H2) * (carr H1)
thus (carr H1) * (carr H2) c= (carr H2) * (carr H1) :: according to XBOOLE_0:def 10 :: thesis: (carr H2) * (carr H1) c= (carr H1) * (carr H2)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H1) * (carr H2) or x in (carr H2) * (carr H1) )
assume A16: x in (carr H1) * (carr H2) ; :: thesis: x in (carr H2) * (carr H1)
then reconsider y = x as Element of G ;
y " in carr H by A15, A16, Th90;
then consider a, b being Element of G such that
A17: ( y " = a * b & a in carr H1 & b in carr H2 ) by A15;
A18: y = (y " ) "
.= (b " ) * (a " ) by A17, GROUP_1:25 ;
( a " in carr H1 & b " in carr H2 ) by A17, Th90;
hence x in (carr H2) * (carr H1) by A18; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H2) * (carr H1) or x in (carr H1) * (carr H2) )
assume A19: x in (carr H2) * (carr H1) ; :: thesis: x in (carr H1) * (carr H2)
then reconsider y = x as Element of G ;
consider a, b being Element of G such that
A20: ( x = a * b & a in carr H2 & b in carr H1 ) by A19;

now

assume A21: not y " in carr H ; :: thesis: contradiction
( y " = (b " ) * (a " ) & a " in carr H2 & b " in carr H1 ) by A20, Th90, GROUP_1:25;
hence contradiction by A15, A21; :: thesis: verum

end;

then (y " ) " in carr H by Th90;
hence x in (carr H1) * (carr H2) by A15; :: thesis: verum