consider N being ExtNat such that
A1: N in X by ThEx;
per cases ( sup X = +infty or sup X <> +infty ) ;
suppose sup X = +infty ; :: thesis: sup X is ext-natural
hence sup X is ext-natural ; :: thesis: verum
end;
suppose A2: sup X <> +infty ; :: thesis: sup X is ext-natural
A3: 0 <= sup X by A1, XXREAL_2:4;
then sup X in REAL by A2, XREAL_0:def 1, XXREAL_0:10;
then reconsider S = sup X as Real ;
set s = [\S/];
now :: thesis: for x being ExtNat st x in X holds
x <= [\S/]
let x be ExtNat; :: thesis: ( x in X implies x <= [\S/] )
assume x in X ; :: thesis: x <= [\S/]
then A4: x <= S by XXREAL_2:4;
then x <> +infty by XXREAL_0:4;
then reconsider n = x as Nat by Th3;
n < [\S/] + 1 by A4, INT_1:29, XXREAL_0:2;
hence x <= [\S/] by INT_1:7; :: thesis: verum
end;
then [\S/] is UpperBound of X by DefU;
then B1: S <= [\S/] by XXREAL_2:def 3;
[\S/] <= S by INT_1:def 6;
hence sup X is ext-natural by A3, B1, XXREAL_0:1; :: thesis: verum
end;
end;