((<%x%> ^ <%y%>) ^ <%z%>) ^ <%t%> is REAL -valued ;
hence <%x,y,z,t%> is REAL -valued by AFINSQ_1:def 14; :: thesis: verum