reconsider Z = the carrier of I[01] as Subset of R^1 by BORSUK_1:1;
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:1;
then reconsider C = A as Subset of R^1 by A1, XBOOLE_1:1;
hereby :: thesis: ( B is closed implies A is closed )
assume A is closed ; :: thesis: B is closed
then A2: C is closed by JORDAN5A:23;
C /\ ([#] I[01]) = B by A1, XBOOLE_1:28;
hence B is closed by A2, PRE_TOPC:13; :: thesis: verum
end;
assume A3: B is closed ; :: thesis: A is closed
Z is closed by Lm1, BORSUK_1:def 11;
then ( B is closed iff C is closed ) by A1, TSEP_1:8;
hence A is closed by A3, JORDAN5A:23; :: thesis: verum