take 0 ; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of {+infty }
let x be ext-real number ; :: according to XXREAL_2:def 2 :: thesis: ( x in {+infty } implies 0 <= x )
assume x in {+infty } ; :: thesis: 0 <= x
hence 0 <= x by TARSKI:def 1; :: thesis: verum