( {0,REAL} in {{0,REAL},{0}} & REAL in {0,REAL} ) by TARSKI:def 2;
hence not -infty in REAL+ by ARYTM_0:1, XREGULAR:7; :: thesis: verum