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 A2: ( seq is bounded_below & seq is bounded_above & - seq is bounded ) ;
( superior_realsequence seq is bounded & inferior_realsequence seq is bounded ) by A1, Th58;
then A3: ( superior_realsequence seq is bounded_below & superior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_above & inferior_realsequence seq is bounded_below ) ;
then A4: - (lim_inf seq) = - (- (inf (- (inferior_realsequence seq)))) by Th13
.= inf (- (- (superior_realsequence (- seq)))) by A2, Th63
.= lim_sup (- seq) ;
- (lim_sup seq) = - (- (sup (- (superior_realsequence seq)))) by A3, Th14
.= sup (- (- (inferior_realsequence (- seq)))) by A2, Th64
.= lim_inf (- seq) ;
hence ( lim_sup (- seq) = - (lim_inf seq) & lim_inf (- seq) = - (lim_sup seq) ) by A4; :: thesis: verum