[s1,t1],[s2,t2] are_connected by BORSUK_2:def 3;
hence pr1 L is Path of s1,s2 by Th13; :: thesis: verum