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