let G be addGroup; :: 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, Th16;
hence - g in (carr H1) + (carr H2) by A7; :: thesis: verum

end;

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, RLVECT_1:def 3
.= (a1 + (b1 + a2)) + b2 by RLVECT_1:def 3 ;
then A21: g1 + g2 = ((a1 + a) + b) + b2 by A17, RLVECT_1:def 3
.= (a1 + a) + (b + b2) by RLVECT_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;

hence ex H being strict Subgroup of G st the carrier of H = (carr H1) + (carr H2) by A2, Th9, 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, Th16 ;
( - 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, Th16, Th75;
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