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