let a be ExtReal; :: thesis: ( a in REAL implies -infty < a )
-infty <= a by Def5, Lm4, Lm6;
hence ( a in REAL implies -infty < a ) by Th1, Th11; :: thesis: verum