let a, b be real number ; :: thesis: for B being Subset of I[01] st B = [.a,b.] holds
B is closed
let B be Subset of I[01] ; :: thesis: ( B = [.a,b.] implies B is closed )
assume A1: B = [.a,b.] ; :: thesis: B is closed
reconsider B2 = B as Subset of R^1 by BORSUK_1:83, TOPMETR:24, XBOOLE_1:1;
A2: B2 is closed by A1, TREAL_1:4;
reconsider I1 = [.0 ,1.] as Subset of R^1 by TOPMETR:24;
A3: [#] (R^1 | I1) = the carrier of I[01] by BORSUK_1:83, PRE_TOPC:def 10;
A4: I[01] = R^1 | I1 by TOPMETR:26, TOPMETR:27;
B = B2 /\ ([#] (R^1 | I1)) by A3, XBOOLE_1:28;
hence B is closed by A2, A4, PRE_TOPC:43; :: thesis: verum