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