:: deftheorem defines <% AFINSQ_1:def 5 :
for x, y being object holds <%x,y%> = <%x%> ^ <%y%>;