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 MEASURE6:40;
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) )
A2: -- (rng seq) c= REAL by MEMBERED:3;
assume A3: x in -- (rng seq) ; :: thesis: x in rng (- seq)
then reconsider r = x as Real by A2;
- r in -- (-- (rng seq)) by A3, MEMBER_1:12;
then - (- r) in rng (- seq) by Th3;
hence x in rng (- seq) ; :: thesis: verum