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