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