let A be non empty Subset of ExtREAL ; :: thesis: ( ( for r being R_eal st r in A holds
r <= -infty ) implies A = {-infty } )
assume A1: for r being R_eal st r in A holds
r <= -infty ; :: thesis: A = {-infty }
assume A <> {-infty } ; :: thesis: contradiction
then consider a being Element of A such that
A2: a <> -infty by Th3;
thus contradiction by A1, A2, XXREAL_0:6; :: thesis: verum