for G being _Graph
for e, x, y being set
for v1 being Vertex of G st x in G .reachableDFrom v1 & e DJoins x,y,G holds
y in G .reachableDFrom v1