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