theorem Th4: :: JGRAPH_1:4

for X being non empty set
for f being FinSequence of X holds PairF f is FinSequence of the carrier' of (PGraph X)