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