take +infty ; :: thesis: for x being ext-real number st x in X holds
x <= +infty
thus for x being ext-real number st x in X holds
x <= +infty by XXREAL_0:4; :: thesis: verum