let X be non empty Subset of REAL ; :: thesis: ( X is bounded_above implies sup X = - (inf (- X)) )
assume X is bounded_above ; :: thesis: sup X = - (inf (- X))
then A1: - X is bounded_below by Lm1;
set r = - (inf (- X));

A2: now

let t be real number ; :: thesis: ( t in X implies t <= - (inf (- X)) )
assume t in X ; :: thesis: t <= - (inf (- X))
then - t in - X ;
then - t >= - (- (inf (- X))) by A1, SEQ_4:def 5;
hence t <= - (inf (- X)) by XREAL_1:26; :: thesis: verum

end;

now

let s be real number ; :: thesis: ( ( for t being real number st t in X holds
t <= s ) implies - (inf (- X)) <= s )
assume A3: for t being real number st t in X holds
t <= s ; :: thesis: - (inf (- X)) <= s

now

let t be real number ; :: thesis: ( t in - X implies t >= - s )
assume t in - X ; :: thesis: t >= - s
then - t in - (- X) ;
then - t <= s by A3;
then - (- t) >= - s by XREAL_1:26;
hence t >= - s ; :: thesis: verum

end;

then - (- (inf (- X))) >= - s by SEQ_4:60;
hence - (inf (- X)) <= s by XREAL_1:26; :: thesis: verum

end;

hence sup X = - (inf (- X)) by A2, SEQ_4:63; :: thesis: verum