r in REAL by XREAL_0:def 1;
hence Im r is zero by Def2; :: thesis: verum