set ff = MeetTBA (T,x);

for a, b being Element of T holds (MeetTBA (T,x)) . (a,b) = (MeetTBA (T,x)) . (b,a) by ThCom1;

hence MeetTBA (T,x) is commutative by BINOP_1:def 2; :: thesis: verum

for a, b being Element of T holds (MeetTBA (T,x)) . (a,b) = (MeetTBA (T,x)) . (b,a) by ThCom1;

hence MeetTBA (T,x) is commutative by BINOP_1:def 2; :: thesis: verum