A: for s being real number st s in X holds
s <= sup X by XXREAL_2:4;

now

let t be real number ; :: thesis: ( ( for s being real number st s in X holds
t >= s ) implies t >= sup X )
assume Z: for s being real number st s in X holds
t >= s ; :: thesis: t >= sup X
for x being ext-real number st x in X holds
x <= t by Z;
then t is UpperBound of X by XXREAL_2:def 1;
hence t >= sup X by XXREAL_2:def 3; :: thesis: verum

end;

hence upper_bound X = sup X by A, Lm63; :: thesis: verum