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

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

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

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

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

end;

then - (- (upper_bound (-- X))) <= - t by SEQ_4:45;
hence - (upper_bound (-- X)) >= t by XREAL_1:24; :: thesis: verum

end;

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

now :: thesis: for s being Real st s in X holds
s >= - (upper_bound (-- X))

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

end;

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