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