let a be ext-real number ; :: thesis: ( a in REAL implies -infty < a )
-infty <= a by Def5, Lm3, Lm5;
hence ( a in REAL implies -infty < a ) by Th1, Th11; :: thesis: verum