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