:: deftheorem defines satisfying_TT AIMLOOP:def 7 :
for Q being multLoop holds
( Q is satisfying_TT iff for u, x, y being Element of Q holds T_map ((T_map (u,x)),y) = T_map ((T_map (u,y)),x) );