:: deftheorem Def16 defines satisfying_aa2 AIMLOOP:def 16 :
for Q being multLoop holds
( Q is satisfying_aa2 iff for x, y, z, u, w being Element of Q holds a_op (x,(a_op (y,z,u)),w) = 1. Q );