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