:: deftheorem defines <% AFINSQ_1:def 14 :
for x1, x2, x3, x4 being object holds <%x1,x2,x3,x4%> = ((<%x1%> ^ <%x2%>) ^ <%x3%>) ^ <%x4%>;