for G being _Graph
for v1 being Vertex of G
for e, x, y being object st x in G .reachableFrom v1 & e Joins x,y,G holds
y in G .reachableFrom v1 by Lm2;