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

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