let X be ext-real-membered set ; :: thesis: -infty is LowerBound of X
let x be ExtReal; :: according to XXREAL_2:def 2 :: thesis: ( x in X implies -infty <= x )
assume x in X ; :: thesis: -infty <= x
thus -infty <= x by XXREAL_0:5; :: thesis: verum