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