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