take 0 ; :: according to XXREAL_2:def 10 :: thesis: 0 is UpperBound of {-infty }
let x be ext-real number ; :: 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