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