let V be set ; :: thesis: for G2 being _Graph
for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G2 be _Graph; :: thesis: for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let c be Cardinal; :: thesis: for G1 being addVertices of G2,V holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G1 be addVertices of G2,V; :: thesis: ( G1 is c -vcolorable iff G2 is c -vcolorable )

hereby :: thesis: ( G2 is c -vcolorable implies G1 is c -vcolorable )

assume A1: G1 is c -vcolorable ; :: thesis: G2 is c -vcolorable
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is c -vcolorable by A1, Th31; :: thesis: verum

end;

assume G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable
then consider f2 being VColoring of G2 such that
A2: ( f2 is proper & card (rng f2) c= c ) ;
set x = the Element of rng f2;
set h = (V \ (the_Vertices_of G2)) --> the Element of rng f2;
set f1 = f2 +* ((V \ (the_Vertices_of G2)) --> the Element of rng f2);
A3: dom ((V \ (the_Vertices_of G2)) --> the Element of rng f2) = V \ (the_Vertices_of G2) ;
then reconsider f1 = f2 +* ((V \ (the_Vertices_of G2)) --> the Element of rng f2) as VColoring of G1 by Th4;
A4: f1 is proper by A2, A3, Th19;
card (rng f1) c= card (rng f2) by Lm3, CARD_1:11;
hence G1 is c -vcolorable by A2, A4, XBOOLE_1:1; :: thesis: verum