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