theorem Th22: :: GLIB_008:22

for G being _Graph
for v1, v2 being Vertex of G st not v1 in G .reachableFrom v2 holds
G .reachableFrom v1 misses G .reachableFrom v2