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