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

x <= +infty

thus for x being ExtReal st x in X holds

x <= +infty by XXREAL_0:4; :: thesis: verum

x <= +infty

thus for x being ExtReal st x in X holds

x <= +infty by XXREAL_0:4; :: thesis: verum