let X be ext-real-membered set ; :: thesis: ( -infty is UpperBound of X implies X c= {-infty} )
assume A1: -infty is UpperBound of X ; :: thesis: X c= {-infty}
let x be ExtReal; :: 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 A1, Def1, XXREAL_0:6;
hence x in {-infty} by TARSKI:def 1; :: thesis: verum