let X be Subset of REAL ; :: thesis: ( X is closed implies - X is closed )
assume A1: X is closed ; :: thesis: - X is closed
let s1 be Real_Sequence; :: according to RCOMP_1:def 4 :: thesis: ( not proj2 s1 c= - X or not s1 is convergent or lim s1 in - X )
assume that
A2: rng s1 c= - X and
A3: s1 is convergent ; :: thesis: lim s1 in - X
A4: - s1 is convergent by A3, SEQ_2:23;
rng (- s1) c= X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (- s1) or x in X )
assume x in rng (- s1) ; :: thesis: x in X
then consider n being set such that
A5: n in dom (- s1) and
A6: x = (- s1) . n by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A5;
A7: x = - (s1 . n) by A6, SEQ_1:14;
s1 . n in rng s1 by FUNCT_2:6;
then x in - (- X) by A2, A7;
hence x in X ; :: thesis: verum

end;

then A8: lim (- s1) in X by A1, A4, RCOMP_1:def 4;
- (lim s1) = lim (- s1) by A3, SEQ_2:24;
then - (- (lim s1)) in - X by A8;
hence lim s1 in - X ; :: thesis: verum