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