let n be Element of NAT ; :: thesis: for seq being Real_Sequence st seq is bounded_below holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
let seq be Real_Sequence; :: thesis: ( seq is bounded_below implies (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) )
assume seq is bounded_below ; :: thesis: (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)
then A1: ( - seq is bounded_above & seq ^\ n is bounded_below ) by Th27;
(inferior_realsequence seq) . n = inf (seq ^\ n) by Th38
.= - (sup (- (seq ^\ n))) by A1, Th14
.= - (sup ((- seq) ^\ n)) by SEQM_3:38 ;
hence (inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n) by Th39; :: thesis: verum