let X be ext-real-membered set ; :: thesis: +infty is UpperBound of X

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= +infty )

assume x in X ; :: thesis: x <= +infty

thus x <= +infty by XXREAL_0:3; :: thesis: verum

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in X implies x <= +infty )

assume x in X ; :: thesis: x <= +infty

thus x <= +infty by XXREAL_0:3; :: thesis: verum