not REAL in REAL ;
hence not +infty is real ; :: thesis: verum