theorem Th3: :: RINFSUP1:3

for r being Real
for seq being Real_Sequence holds
( r in rng seq iff - r in rng (- seq) )