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