set T = I[01] | {0[01] };
0[01] in {0[01] } by TARSKI:def 1;
then reconsider nl = 0[01] as Point of (I[01] | {0[01] }) by PRE_TOPC:29;
A1: the carrier of (I[01] | {0[01] }) = {0[01] } by PRE_TOPC:29;
for a, b being Point of (I[01] | {0[01] }) holds a,b are_connected

proof

reconsider f = I[01] --> nl as Function of I[01] ,(I[01] | {0[01] }) ;
let a, b be Point of (I[01] | {0[01] }); :: thesis: a,b are_connected
take f ; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = a & f . 1 = b )
thus f is continuous ; :: thesis: ( f . 0 = a & f . 1 = b )
( a = nl & b = nl ) by A1, TARSKI:def 1;
hence ( f . 0 = a & f . 1 = b ) by BORSUK_1:def 18, FUNCOP_1:13; :: thesis: verum

end;

then I[01] | {0[01] } is pathwise_connected by Def3;
hence ex b₁ being TopSpace st
( b₁ is strict & b₁ is pathwise_connected & not b₁ is empty ) ; :: thesis: verum