theorem Th60: :: RINFSUP1:60

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