assume +infty in [:{0 },REAL+ :] ; :: thesis: contradiction
then +infty in REAL+ \/ [:{0 },REAL+ :] by XBOOLE_0:def 3;
then +infty in REAL by Lm1, ZFMISC_1:64;
hence contradiction ; :: thesis: verum