let a, b be Real; :: 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:40, TOPMETR:17, XBOOLE_1:1;
A2: B2 is closed by A1, TREAL_1:1;
reconsider I1 = [.0,1.] as Subset of R^1 by TOPMETR:17;
A3: [#] (R^1 | I1) = the carrier of I[01] by BORSUK_1:40, PRE_TOPC:def 5;
A4: I[01] = R^1 | I1 by TOPMETR:19, TOPMETR:20;
B = B2 /\ ([#] (R^1 | I1)) by A3, XBOOLE_1:28;
hence B is closed by A2, A4, PRE_TOPC:13; :: thesis: verum