let x, y be Element of (RAdj (R,T)); :: thesis:
reconsider a = x, b = y as Element of S by Lm10;
thus x * y = a * b by Lm12
.= b * a by GROUP_1:def 12
.= y * x by Lm12 ; :: thesis:

end;