theorem :: XXREAL_2:92

for A being non empty Subset of ExtREAL st ( for r being Element of ExtREAL st r in A holds
r <= -infty ) holds
A = {-infty}