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