( s1,s2 are_connected & t1,t2 are_connected ) by BORSUK_2:def 3;
hence <:L1,L2:> is Path of [s1,t1],[s2,t2] by Th16; :: thesis: verum