theorem :: GRAPH_5:57

for G being finite Graph
for ps being oriented Simple Chain of G holds len ps <= VerticesCount G