take
0
; :: according to XXREAL_2:def 9 :: thesis: 0 is LowerBound of {+infty}

let x be ExtReal; :: 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

let x be ExtReal; :: 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