a,b are_connected by Def3;
hence for P being Path of a,b holds (T,a,b,b₁,b₁) by Th12; :: thesis: verum