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