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