let X, V be set ; :: thesis: 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 )
let G be Graph; :: thesis: 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 )
let pe, qe be FinSequence of the carrier' of G; :: thesis: ( (vertices (pe ^ qe)) \ X c= V implies ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) )
A1: ( rng pe c= rng (pe ^ qe) & rng qe c= rng (pe ^ qe) ) by FINSEQ_1:29, FINSEQ_1:30;
assume (vertices (pe ^ qe)) \ X c= V ; :: thesis: ( (vertices pe) \ X c= V & (vertices qe) \ X c= V )
hence ( (vertices pe) \ X c= V & (vertices qe) \ X c= V ) by A1, Th20; :: thesis: verum