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