assume A1: -infty in REAL+ ; :: thesis: contradiction
A2: {0 ,REAL } in -infty by TARSKI:def 2;
REAL in {0 ,REAL } by TARSKI:def 2;
hence contradiction by A1, A2, ARYTM_0:1, ORDINAL1:3; :: thesis: verum