let S, T be non empty TopSpace; for s1, s2 being Point of S
for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
s1,s2 are_connected
let s1, s2 be Point of S; for t1, t2 being Point of T st [s1,t1],[s2,t2] are_connected holds
s1,s2 are_connected
let t1, t2 be Point of T; ( [s1,t1],[s2,t2] are_connected implies s1,s2 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]
; BORSUK_2:def 1 s1,s2 are_connected
take f = pr1 L; BORSUK_2:def 1 ( f is continuous & f . 0 = s1 & f . 1 = s2 )
thus
f is continuous
by A1, Th9; ( f . 0 = s1 & f . 1 = s2 )
A4:
( dom f = the carrier of I[01] & dom f = dom L )
by FUNCT_2:def 1, MCART_1:def 12;
then
j0 in dom L
;
hence f . 0 =
[s1,t1] `1
by A2, MCART_1:def 12
.=
s1
;
f . 1 = s2
j1 in dom L
by A4;
hence f . 1 =
[s2,t2] `1
by A3, MCART_1:def 12
.=
s2
;
verum