:: deftheorem defines <% AFINSQ_1:def 1 :
for x being object holds <%x%> = 0 .--> x;