:: deftheorem defines <% PCS_0:def 37 :
for p, q being set holds <%p,q%> = <%p,q%>;