let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies inf seq = - (sup (- seq)) )
assume seq is bounded_below ; :: thesis: inf seq = - (sup (- seq))
then ( not rng seq is empty & rng seq is bounded_below ) by Th6, RELAT_1:64;
then inf (rng seq) = - (sup (- (rng seq))) by PSCOMP_1:17
.= - (sup (rng (- seq))) by Th4 ;
hence inf seq = - (sup (- seq)) ; :: thesis: verum