let A be Subset of REAL ; :: thesis: for B being Subset of R^1 st A = B holds
( A is closed iff B is closed )
let B be Subset of R^1 ; :: thesis: ( A = B implies ( A is closed iff B is closed ) )
assume A1: A = B ; :: thesis: ( A is closed iff B is closed )
thus ( A is closed implies B is closed ) :: thesis: ( B is closed implies A is closed )

proof

assume A is closed ; :: thesis: B is closed
then (A ` ) ` is closed ;
then A ` is open by RCOMP_1:def 5;
then A ` in Family_open_set RealSpace by JORDAN5A:6;
hence ([#] R^1 ) \ B is open by A1, Lm2, PRE_TOPC:def 5, TOPMETR:24; :: according to PRE_TOPC:def 6 :: thesis: verum

end;

assume B is closed ; :: thesis: A is closed
then B ` in the topology of R^1 by PRE_TOPC:def 5;
then A ` is open by A1, Lm2, JORDAN5A:6, TOPMETR:24;
then (A ` ) ` is closed by RCOMP_1:def 5;
hence A is closed ; :: thesis: verum