set ff = JoinTBA (T,x);
for a, b being Element of T holds (JoinTBA (T,x)) . (a,b) = (JoinTBA (T,x)) . (b,a) by ThCom;
hence JoinTBA (T,x) is commutative by BINOP_1:def 2; :: thesis: verum