let U be ExtReal; :: thesis: ( U is UpperBound of X iff for N being ExtNat st N in X holds
N <= U )
thus ( U is UpperBound of X implies for N being ExtNat st N in X holds
N <= U ) by XXREAL_2:def 1; :: thesis: ( ( for N being ExtNat st N in X holds
N <= U ) implies U is UpperBound of X )
assume for N being ExtNat st N in X holds
N <= U ; :: thesis: U is UpperBound of X
then for x being ExtReal st x in X holds
x <= U ;
hence U is UpperBound of X by XXREAL_2:def 1; :: thesis: verum