<%A,x,y%> . 0 = A ;
hence not <%A,x,y%> is natural-valued ; :: thesis: verum