set ff = JoinTBA (T,x);

for a, b, c being Element of T holds (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c))) by ThAssoc;

hence JoinTBA (T,x) is associative by BINOP_1:def 3; :: thesis: verum

for a, b, c being Element of T holds (JoinTBA (T,x)) . (((JoinTBA (T,x)) . (a,b)),c) = (JoinTBA (T,x)) . (a,((JoinTBA (T,x)) . (b,c))) by ThAssoc;

hence JoinTBA (T,x) is associative by BINOP_1:def 3; :: thesis: verum