assume -infty in [:{0 },REAL+ :] ; :: thesis: contradiction
then REAL in REAL+ by ZFMISC_1:106;
hence contradiction by ARYTM_0:1, ORDINAL1:7; :: thesis: verum