let X be ext-natural-membered set ; :: thesis: ( not X is empty & X is bounded_above implies X is right_end )
assume A1: ( not X is empty & X is bounded_above ) ; :: thesis: X is right_end
then consider N being ExtNat such that
A2: N in X by ThEx;

per cases ( X is trivial or not X is trivial ) ;

suppose X is trivial ; :: thesis: X is right_end

hence X is right_end by A2; :: thesis: verum

end;

suppose A3: not X is trivial ; :: thesis: X is right_end

defpred S₁[ Nat] means c₁ in X;
A4: ex n being Nat st S₁[n]

proof

per cases ( N is Nat or N = +infty ) by Th3;

suppose N is Nat ; :: thesis: ex n being Nat st S₁[n]

then reconsider n = N as Nat ;
take n ; :: thesis: S₁[n]
thus S₁[n] by A2; :: thesis: verum

end;

suppose A5: N = +infty ; :: thesis: ex n being Nat st S₁[n]

set n = the Element of X \ {N};
not X \ {N} is empty by A3, ZFMISC_1:139;
then A6: ( the Element of X \ {N} in X & the Element of X \ {N} <> +infty ) by A5, ZFMISC_1:56;
then reconsider n = the Element of X \ {N} as Nat by Th3;
take n ; :: thesis: S₁[n]
thus S₁[n] by A6; :: thesis: verum

end;

end;

end;

consider R being Real such that
B1: R is UpperBound of X by A1, XXREAL_2:def 10;
set r = [\R/];
C2: 0 <= R by A2, B1, XXREAL_2:def 1;
C3: R < [\R/] + 1 by INT_1:29;
then 0 <= [\R/] by C2, INT_1:7;
then [\R/] in NAT by ORDINAL1:def 12;
then reconsider r = [\R/] as Nat ;
B2: for n being Nat st S₁[n] holds
n <= r

proof

let n be Nat; :: thesis: ( S₁[n] implies n <= r )
assume S₁[n] ; :: thesis: n <= r
then n <= R by B1, XXREAL_2:def 1;
then n < r + 1 by C3, XXREAL_0:2;
hence n <= r by NAT_1:13; :: thesis: verum

end;

consider n being Nat such that
A7: ( S₁[n] & ( for m being Nat st S₁[m] holds
m <= n ) ) from NAT_1:sch 6(B2, A4);

now :: thesis: for x being ExtNat st x in X holds
x <= n

let x be ExtNat; :: thesis: ( x in X implies x <= n )
assume A7a: x in X ; :: thesis: x <= n
then x <= R by B1, XXREAL_2:def 1;
then x in REAL by XREAL_0:def 1, XXREAL_0:13;
then x is Nat by Th3;
hence x <= n by A7, A7a; :: thesis: verum

end;

then A8: n is UpperBound of X by DefU;
for x being UpperBound of X holds n <= x by A7, XXREAL_2:def 1;
then sup X = n by A8, XXREAL_2:def 3;
hence X is right_end by A7, XXREAL_2:def 6; :: thesis: verum

end;

end;