theorem Th9: :: GRAPH_5:11
for p, q being FinSequence
for G being Graph st p ^ q is oriented Chain of G holds
( p is oriented Chain of G & q is oriented Chain of G )