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

A2: now

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

end;

now

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

now

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

end;

then - (- (sup (- X))) <= - t by SEQ_4:62;
hence - (sup (- X)) >= t by XREAL_1:26; :: thesis: verum

end;

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