set T = I[01] | {0[01] };
A1: the carrier of (I[01] | {0[01] }) = {0[01] } by PRE_TOPC:29;
( 0[01] in the carrier of I[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;
for a, b being Point of (I[01] | {0[01] }) holds a,b are_connected

proof

let a, b be Point of (I[01] | {0[01] }); :: thesis: a,b are_connected
A2: ( a = nl & b = nl ) by A1, TARSKI:def 1;
reconsider f = I[01] --> nl as Function of I[01] ,(I[01] | {0[01] }) ;
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 )
thus ( f . 0 = a & f . 1 = b ) by A2, BORSUK_1:def 18, FUNCOP_1:13; :: thesis: verum

end;

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