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 the topology of R^1 by Lm8, Th5;
hence ([#] R^1) \ B is open by A1, TOPMETR:17; :: according to PRE_TOPC:def 3 :: thesis: verum
end;
assume B is closed ; :: thesis: A is closed
then B ` in the topology of R^1 by PRE_TOPC:def 2;
then A ` is open by A1, Lm8, Th5, TOPMETR:17;
then (A `) ` is closed by RCOMP_1:def 5;
hence A is closed ; :: thesis: verum