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