REAL in {REAL } by TARSKI:def 1;
hence REAL is Point of by Lm3; :: thesis: verum