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 rng 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: - (lim s1) = lim (- s1) by A3, SEQ_2:10;
A5: rng (- s1) c= X

proof

let x be object ; :: 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 object such that
A6: n in dom (- s1) and
A7: x = (- s1) . n by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A6;
A8: s1 . n in rng s1 by FUNCT_2:4;
x = - (s1 . n) by A7, SEQ_1:10;
then x in -- (-- X) by A2, A8;
hence x in X ; :: thesis: verum

end;

- s1 is convergent by A3;
then lim (- s1) in X by A1, A5;
then - (- (lim s1)) in -- X by A4;
hence lim s1 in -- X ; :: thesis: verum