assume +infty in REAL ; :: according to XREAL_0:def 1 :: thesis: contradiction
hence contradiction ; :: thesis: verum