let T be non empty TopSpace; :: thesis: for a being Point of T holds I[01] --> a is Path of a,a
let a be Point of T; :: thesis: I[01] --> a is Path of a,a
thus a,a are_connected ; :: according to BORSUK_2:def 2 :: thesis: ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a )
thus ( I[01] --> a is continuous & (I[01] --> a) . 0 = a & (I[01] --> a) . 1 = a ) by BORSUK_1:def 14, BORSUK_1:def 15, TOPALG_3:4; :: thesis: verum