let A be non empty Subset of ExtREAL ; :: thesis: ( ( for r being R_eal st r in A holds
+infty <= r ) implies A = {+infty } )
assume A1: for r being R_eal st r in A holds
+infty <= r ; :: thesis: A = {+infty }
assume A <> {+infty } ; :: thesis: contradiction
then ex a being Element of A st a <> +infty by Th3;
hence contradiction by A1, XXREAL_0:4; :: thesis: verum