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