let P be Subset of I[01]; :: thesis: ( P = the carrier of I[01] \ {0,1} implies P is open )

assume A1: P = the carrier of I[01] \ {0,1} ; :: thesis: P is open

A2: 0 in [.0,1.] by XXREAL_1:1;

A3: 1 in [.0,1.] by XXREAL_1:1;

reconsider Q0 = {0} as Subset of I[01] by A2, BORSUK_1:40, ZFMISC_1:31;

reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1:40, ZFMISC_1:31;

Q0 \/ Q1 is closed by A2, A3, BORSUK_1:40, TOPS_1:9;

then ([#] I[01]) \ (Q0 \/ Q1) is open ;

hence P is open by A1, ENUMSET1:1; :: thesis: verum

assume A1: P = the carrier of I[01] \ {0,1} ; :: thesis: P is open

A2: 0 in [.0,1.] by XXREAL_1:1;

A3: 1 in [.0,1.] by XXREAL_1:1;

reconsider Q0 = {0} as Subset of I[01] by A2, BORSUK_1:40, ZFMISC_1:31;

reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1:40, ZFMISC_1:31;

Q0 \/ Q1 is closed by A2, A3, BORSUK_1:40, TOPS_1:9;

then ([#] I[01]) \ (Q0 \/ Q1) is open ;

hence P is open by A1, ENUMSET1:1; :: thesis: verum