theorem Th6: :: MSSCYC_1:7

for G being Graph
for e being set st e in the carrier' of G holds
for fe being directed Chain of G st fe = <*e*> holds
vertex-seq fe = <*( the Source of G . e),( the Target of G . e)*>