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: now :: thesis: for g being Element of G st g in (carr H1) * (carr H2) holds
g " in (carr H1) * (carr H2)

let g be Element of G; :: thesis: ( g in (carr H1) * (carr H2) implies g " in (carr H1) * (carr H2) )
assume A3: g in (carr H1) * (carr H2) ; :: thesis: g " in (carr H1) * (carr H2)
then consider a, b being Element of G such that
A4: g = a * b and
a in carr H1 and
b in carr H2 ;
consider b1, a1 being Element of G such that
A5: a * b = b1 * a1 and
A6: ( b1 in carr H2 & a1 in carr H1 ) by A1, A3, A4;
A7: ( a1 " in carr H1 & b1 " in carr H2 ) by A6, Th75;
g " = (a1 ") * (b1 ") by A4, A5, GROUP_1:17;
hence g " in (carr H1) * (carr H2) by A7; :: thesis: verum

end;

A8: now :: thesis: for g1, g2 being Element of G st g1 in (carr H1) * (carr H2) & g2 in (carr H1) * (carr H2) holds
g1 * g2 in (carr H1) * (carr H2)

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
A9: g1 in (carr H1) * (carr H2) and
A10: g2 in (carr H1) * (carr H2) ; :: thesis: g1 * g2 in (carr H1) * (carr H2)
consider a1, b1 being Element of G such that
A11: g1 = a1 * b1 and
A12: a1 in carr H1 and
A13: b1 in carr H2 by A9;
consider a2, b2 being Element of G such that
A14: g2 = a2 * b2 and
A15: a2 in carr H1 and
A16: b2 in carr H2 by A10;
b1 * a2 in (carr H1) * (carr H2) by A1, A13, A15;
then consider a, b being Element of G such that
A17: b1 * a2 = a * b and
A18: a in carr H1 and
A19: b in carr H2 ;
A20: b * b2 in carr H2 by A16, A19, Th74;
g1 * g2 = ((a1 * b1) * a2) * b2 by A11, A14, GROUP_1:def 3
.= (a1 * (b1 * a2)) * b2 by GROUP_1:def 3 ;
then A21: g1 * g2 = ((a1 * a) * b) * b2 by A17, GROUP_1:def 3
.= (a1 * a) * (b * b2) by GROUP_1:def 3 ;
a1 * a in carr H1 by A12, A18, Th74;
hence g1 * g2 in (carr H1) * (carr H2) by A21, A20; :: thesis: verum

end;

(carr H1) * (carr H2) <> {} by Th9;
hence ex H being strict Subgroup of G st the carrier of H = (carr H1) * (carr H2) by A8, A2, Th52; :: thesis: verum

end;

given H being Subgroup of G such that A22: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H1) * (carr H2) or x in (carr H2) * (carr H1) )
assume A23: 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 A22, A23, Th75;
then consider a, b being Element of G such that
A24: y " = a * b and
A25: ( a in carr H1 & b in carr H2 ) by A22;
A26: y = (y ") "
.= (b ") * (a ") by A24, GROUP_1:17 ;
( a " in carr H1 & b " in carr H2 ) by A25, Th75;
hence x in (carr H2) * (carr H1) by A26; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (carr H2) * (carr H1) or x in (carr H1) * (carr H2) )
assume A27: 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
A28: ( x = a * b & a in carr H2 ) and
A29: b in carr H1 by A27;

now :: thesis: y " in carr H

A30: b " in carr H1 by A29, Th75;
assume A31: not y " in carr H ; :: thesis: contradiction
( y " = (b ") * (a ") & a " in carr H2 ) by A28, Th75, GROUP_1:17;
hence contradiction by A22, A31, A30; :: thesis: verum

end;

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