:: deftheorem Def21 defines satisfying_aK3 AIMLOOP:def 21 :
for Q being multLoop holds
( Q is satisfying_aK3 iff for x, y, z, u being Element of Q holds a_op (x,y,(K_op (z,u))) = 1. Q );