theorem :: XXREAL_2:93

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