for T being _Tree
for a, b being Vertex of T
for P1, P2 being Path of T st P1 is_Walk_from a,b & P2 is_Walk_from a,b holds
P1 = P2