let X be non empty Subset of REAL; :: thesis: ( X is bounded_above implies upper_bound X = - (lower_bound (-- X)) )
set r = - (lower_bound (-- X));

A1: now :: thesis: for s being Real st ( for t being Real st t in X holds
t <= s ) holds
- (lower_bound (-- X)) <= s

let s be Real; :: thesis: ( ( for t being Real st t in X holds
t <= s ) implies - (lower_bound (-- X)) <= s )
assume A2: for t being Real st t in X holds
t <= s ; :: thesis: - (lower_bound (-- X)) <= s

now :: thesis: for t being Real st t in -- X holds
t >= - s

let t be Real; :: thesis: ( t in -- X implies t >= - s )
assume t in -- X ; :: thesis: t >= - s
then - t in -- (-- X) ;
then - t <= s by A2;
then - (- t) >= - s by XREAL_1:24;
hence t >= - s ; :: thesis: verum

end;

then - (- (lower_bound (-- X))) >= - s by SEQ_4:43;
hence - (lower_bound (-- X)) <= s by XREAL_1:24; :: thesis: verum

end;

assume X is bounded_above ; :: thesis: upper_bound X = - (lower_bound (-- X))
then A3: -- X is bounded_below by Lm2;

now :: thesis: for t being Real st t in X holds
t <= - (lower_bound (-- X))

let t be Real; :: thesis: ( t in X implies t <= - (lower_bound (-- X)) )
assume t in X ; :: thesis: t <= - (lower_bound (-- X))
then - t in -- X ;
then - t >= - (- (lower_bound (-- X))) by A3, SEQ_4:def 2;
hence t <= - (lower_bound (-- X)) by XREAL_1:24; :: thesis: verum

end;

hence upper_bound X = - (lower_bound (-- X)) by A1, SEQ_4:46; :: thesis: verum