A1: now :: thesis: for t being Real st ( for s being Real st s in X holds
t >= s ) holds
t >= sup X

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

end;

for s being Real st s in X holds
s <= sup X by XXREAL_2:4;
hence upper_bound X = sup X by A1, Lm2; :: thesis: verum