theorem Th59: :: RINFSUP1:59

for n being Nat
for seq being Real_Sequence st seq is bounded_below holds
(inferior_realsequence seq) . n = - ((superior_realsequence (- seq)) . n)