let a, b be Real; for B being Subset of I[01] st B = [.a,b.] holds
B is closed
let B be Subset of I[01]; ( B = [.a,b.] implies B is closed )
assume A1:
B = [.a,b.]
; 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; verum