let A be non empty Subset of ExtREAL; :: thesis: ( ( for r being Element of ExtREAL st r in A holds

+infty <= r ) implies A = {+infty} )

assume A1: for r being Element of ExtREAL 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 SETFAM_1:49;

hence contradiction by A1, XXREAL_0:4; :: thesis: verum

+infty <= r ) implies A = {+infty} )

assume A1: for r being Element of ExtREAL 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 SETFAM_1:49;

hence contradiction by A1, XXREAL_0:4; :: thesis: verum