let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies lower_bound seq = - (upper_bound (- seq)) )
assume seq is bounded_below ; :: thesis: lower_bound seq = - (upper_bound (- seq))
then ( not rng seq is empty & rng seq is bounded_below ) by Th6, RELAT_1:41;
then lower_bound (rng seq) = - (upper_bound (-- (rng seq))) by MEASURE6:43
.= - (upper_bound (rng (- seq))) by Th4 ;
hence lower_bound seq = - (upper_bound (- seq)) ; :: thesis: verum