take
-infty
; :: thesis: for x being ExtReal st x in X holds

-infty <= x

thus for x being ExtReal st x in X holds

-infty <= x by XXREAL_0:5; :: thesis: verum

-infty <= x

thus for x being ExtReal st x in X holds

-infty <= x by XXREAL_0:5; :: thesis: verum