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