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