x in REAL by XREAL_0:def 1;
hence <%x%> is REAL -valued ; :: thesis: verum