assume
-infty in [:{0},REAL+:]
; :: thesis: contradiction

then REAL in REAL+ by ZFMISC_1:87;

hence contradiction by ARYTM_0:1, ORDINAL1:5; :: thesis: verum

then REAL in REAL+ by ZFMISC_1:87;

hence contradiction by ARYTM_0:1, ORDINAL1:5; :: thesis: verum