let X be ext-real-membered set ; :: thesis: ( -infty is UpperBound of X implies X c= {-infty } )
assume Z: -infty is UpperBound of X ; :: thesis: X c= {-infty }
let x be ext-real number ; :: according to MEMBERED:def 8 :: thesis: ( not x in X or x in {-infty } )
assume x in X ; :: thesis: x in {-infty }
then x = -infty by Z, Def1, XXREAL_0:6;
hence x in {-infty } by TARSKI:def 1; :: thesis: verum