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