let T be non empty TopSpace; :: thesis: for a being Point of T ex f being Function of I[01] ,T st
( f is continuous & f . 0 = a & f . 1 = a )
let a be Point of T; :: thesis: ex f being Function of I[01] ,T st
( f is continuous & f . 0 = a & f . 1 = a )
take IT = I[01] --> a; :: thesis: ( IT is continuous & IT . 0 = a & IT . 1 = a )
thus IT is continuous ; :: thesis: ( IT . 0 = a & IT . 1 = a )
thus ( IT . 0 = a & IT . 1 = a ) by BORSUK_1:def 17, BORSUK_1:def 18, FUNCOP_1:13; :: thesis: verum