let seq be Real_Sequence; :: thesis: rng (- seq) = - (rng seq)
thus rng (- seq) c= - (rng seq) :: according to XBOOLE_0:def 10 :: thesis: - (rng seq) c= rng (- seq)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (- seq) or x in - (rng seq) )
assume A1: x in rng (- seq) ; :: thesis: x in - (rng seq)
then reconsider r = x as Real ;
- r in rng (- (- seq)) by A1, Th3;
then - (- r) in - (rng seq) by PSCOMP_1:14;
hence x in - (rng seq) ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in - (rng seq) or x in rng (- seq) )
assume A2: x in - (rng seq) ; :: thesis: x in rng (- seq)
then reconsider r = x as Real ;
- r in - (- (rng seq)) by A2, PSCOMP_1:14;
then - (- r) in rng (- seq) by Th3;
hence x in rng (- seq) ; :: thesis: verum