theorem Th54: :: GLIB_006:50

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