set ff = MeetTBA (T,x);
for a, b, c being Element of T holds (MeetTBA (T,x)) . (((MeetTBA (T,x)) . (a,b)),c) = (MeetTBA (T,x)) . (a,((MeetTBA (T,x)) . (b,c))) by ThV2;
hence MeetTBA (T,x) is associative by BINOP_1:def 3; :: thesis: verum