:: deftheorem defines satisfying_LL AIMLOOP:def 11 :
for Q being multLoop holds
( Q is satisfying_LL iff for u, x, y, z, w being Element of Q holds L_map ((L_map (u,x,y)),z,w) = L_map ((L_map (u,z,w)),x,y) );