theorem Th3: :: MSSCYC_1:4

for G being Graph
for e being set
for s, t being Element of the carrier of G st s = the Source of G . e & t = the Target of G . e holds
<*s,t*> is_vertex_seq_of <*e*>