let S, T be non empty TopSpace; :: thesis: for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
t1,t2 are_connected
let s1, s2 be Point of S; :: thesis: for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
t1,t2 are_connected
let t1, t2 be Point of T; :: thesis: ( [s1,t1],[s2,t2] are_connected implies t1,t2 are_connected )
given L being Function of I[01],[:S,T:] such that A1: L is continuous and
A2: L . 0 = [s1,t1] and
A3: L . 1 = [s2,t2] ; :: according to BORSUK_2:def 1 :: thesis: t1,t2 are_connected
take f = pr2 L; :: according to BORSUK_2:def 1 :: thesis: ( f is continuous & f . 0 = t1 & f . 1 = t2 )
thus f is continuous by A1, Th10; :: thesis: ( f . 0 = t1 & f . 1 = t2 )
A4: ( dom f = the carrier of I[01] & dom f = dom L ) by FUNCT_2:def 1, MCART_1:def 13;
then j0 in dom L ;
hence f . 0 = [s1,t1] `2 by A2, MCART_1:def 13
.= t1 ;
:: thesis: f . 1 = t2
j1 in dom L by A4;
hence f . 1 = [s2,t2] `2 by A3, MCART_1:def 13
.= t2 ;
:: thesis: verum