theorem Th4: :: GLPACY00:2

for G being _Graph
for T being Trail of G holds T .length() = card (T .edges())