let A be non empty Subset of ExtREAL; :: thesis: ( ( for r being Element of ExtREAL st r in A holds
r <= -infty ) implies A = {-infty} )
assume A1: for r being Element of ExtREAL st r in A holds
r <= -infty ; :: 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:6; :: thesis: verum