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:8;

A1: the carrier of (I[01] | {0[01]}) = {0[01]} by PRE_TOPC:8;

for a, b being Point of (I[01] | {0[01]}) holds a,b are_connected

hence ex b_{1} being TopSpace st

( b_{1} is strict & b_{1} is pathwise_connected & not b_{1} is empty )
; :: thesis: verum

0[01] in {0[01]} by TARSKI:def 1;

then reconsider nl = 0[01] as Point of (I[01] | {0[01]}) by PRE_TOPC:8;

A1: the carrier of (I[01] | {0[01]}) = {0[01]} by PRE_TOPC:8;

for a, b being Point of (I[01] | {0[01]}) holds a,b are_connected

proof

then
I[01] | {0[01]} is pathwise_connected
;
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 15, FUNCOP_1:7; :: thesis: verum

end;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 15, FUNCOP_1:7; :: thesis: verum

hence ex b

( b