let seq be Real_Sequence; :: thesis: ( seq is bounded implies ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) )
assume A1: seq is bounded ; :: thesis: ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) )
then inferior_realsequence seq is bounded by Th56;
then A2: - (lim_inf seq) = - (- (lower_bound (- (inferior_realsequence seq)))) by Th13
.= lower_bound (- (- (superior_realsequence (- seq)))) by A1, Th61
.= lim_sup (- seq) ;
superior_realsequence seq is bounded by A1, Th56;
then - (lim_sup seq) = - (- (upper_bound (- (superior_realsequence seq)))) by Th14
.= upper_bound (- (- (inferior_realsequence (- seq)))) by A1, Th62
.= lim_inf (- seq) ;
hence ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) by A2; :: thesis: verum