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

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