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

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