take
0
; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of {-infty}

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in {-infty} implies x <= 0 )

assume x in {-infty} ; :: thesis: x <= 0

hence x <= 0 by TARSKI:def 1; :: thesis: verum

let x be ExtReal; :: according to XXREAL_2:def 1 :: thesis: ( x in {-infty} implies x <= 0 )

assume x in {-infty} ; :: thesis: x <= 0

hence x <= 0 by TARSKI:def 1; :: thesis: verum