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:83, ZFMISC_1:37;
reconsider Q1 = {1} as Subset of I[01] by A3, BORSUK_1:83, ZFMISC_1:37;
Q0 \/ Q1 is closed by A2, A3, BORSUK_1:83, TOPS_1:36;
then ([#] I[01] ) \ (Q0 \/ Q1) is open by PRE_TOPC:def 6;
hence P is open by A1, ENUMSET1:41; :: thesis: verum