let G be Group; :: thesis: (1). G is commutative
let a, b be Element of ((1). G); :: according to GROUP_1:def 12 :: thesis: a * b = b * a
a in the carrier of ((1). G) ;
then a in {(1_ G)} by GROUP_2:def 7;
then A1: a = 1_ G by TARSKI:def 1;
b in the carrier of ((1). G) ;
then b in {(1_ G)} by GROUP_2:def 7;
hence a * b = b * a by A1, TARSKI:def 1; :: thesis: verum