let R be commutative Ring; :: thesis: UnitGroup R is commutative
for x, y being Element of (UnitGroup R) holds x * y = y * x

proof

let x, y be Element of (UnitGroup R); :: thesis: x * y = y * x
( x in units R & y in units R ) ;
then reconsider X = x, Y = y as Element of R ;
thus x * y = X * Y by Th110
.= y * x by Th110 ; :: thesis: verum

end;

hence UnitGroup R is commutative by GROUP_1:def 12; :: thesis: verum