let A be Subset of REAL ; :: thesis: for B being Subset of I[01] st A = B holds
( A is closed iff B is closed )
let B be Subset of I[01] ; :: thesis: ( A = B implies ( A is closed iff B is closed ) )
assume A1: A = B ; :: thesis: ( A is closed iff B is closed )
the carrier of I[01] c= the carrier of R^1 by BORSUK_1:35;
then reconsider C = A as Subset of R^1 by A1, XBOOLE_1:1;
reconsider Z = the carrier of I[01] as Subset of R^1 by BORSUK_1:35;
Z is closed by Lm1, BORSUK_1:def 14;
then A2: ( B is closed iff C is closed ) by A1, TSEP_1:8;

hereby :: thesis: ( B is closed implies A is closed )

assume A is closed ; :: thesis: B is closed
then A3: C is closed by TOPREAL6:79;
C /\ ([#] I[01] ) = B by A1, XBOOLE_1:28;
hence B is closed by A3, PRE_TOPC:43; :: thesis: verum

end;

assume B is closed ; :: thesis: A is closed
hence A is closed by A2, TOPREAL6:79; :: thesis: verum