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
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 15, FUNCOP_1:7; :: thesis: verum
end;
then I[01] | {0[01]} is pathwise_connected ;
hence ex b1 being TopSpace st
( b1 is strict & b1 is pathwise_connected & not b1 is empty ) ; :: thesis: verum