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