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

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