the Path of t1,t2 in Paths (t1,t2) by Def1;
hence not Paths (t1,t2) is empty ; :: thesis: verum