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) )