for x being ExtReal st x in X holds
x <= +infty by XXREAL_0:3;
then reconsider L = +infty as UpperBound of X by XXREAL_2:def 1;
take L ; :: thesis: L is ext-natural
thus L is ext-natural ; :: thesis: verum