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