a,b are_connected by Def3;
hence for b₁ being Function of I[01],T holds
( b₁ is Path of a,b iff ( b₁ is continuous & b₁ . 0 = a & b₁ . 1 = b ) ) by Def2; :: thesis: verum