theorem Th24: :: GRAPH_5:26

for G being Graph
for pe, qe being FinSequence of the carrier' of G holds
( vertices pe c= vertices (pe ^ qe) & vertices qe c= vertices (pe ^ qe) )