let V be set ; :: thesis: for G2 being _Graph
for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -tcolorable iff G2 is c -tcolorable )
let G2 be _Graph; :: thesis: for c being Cardinal
for G1 being addVertices of G2,V holds
( G1 is c -tcolorable iff G2 is c -tcolorable )
let c be Cardinal; :: thesis: for G1 being addVertices of G2,V holds
( G1 is c -tcolorable iff G2 is c -tcolorable )
let G1 be addVertices of G2,V; :: thesis: ( G1 is c -tcolorable iff G2 is c -tcolorable )
G2 is Subgraph of G1 by GLIB_006:57;
hence ( G1 is c -tcolorable implies G2 is c -tcolorable ) by Th166; :: thesis: ( G2 is c -tcolorable implies G1 is c -tcolorable )
assume G2 is c -tcolorable ; :: thesis: G1 is c -tcolorable
then consider t2 being TColoring of G2 such that
A1: ( t2 is proper & card ((rng (t2 _V)) \/ (rng (t2 _E))) c= c ) ;
set x = the Element of rng (t2 _V);
set h = (V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V);
set f = (t2 _V) +* ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V));
A2: dom ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V)) = V \ (the_Vertices_of G2) ;
then reconsider t1 = [((t2 _V) +* ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V))),(t2 _E)] as TColoring of G1 by Th139;
( t1 _E = t2 _E & t1 _V = (t2 _V) +* ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V)) ) ;
then A3: t1 is proper by A1, A2, Th154;
(rng ((t2 _V) +* ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V)))) \/ (rng (t1 _E)) c= (rng (t2 _V)) \/ (rng (t2 _E)) by Lm3, XBOOLE_1:9;
then card ((rng ((t2 _V) +* ((V \ (the_Vertices_of G2)) --> the Element of rng (t2 _V)))) \/ (rng (t1 _E))) c= card ((rng (t2 _V)) \/ (rng (t2 _E))) by CARD_1:11;
hence G1 is c -tcolorable by A1, A3, XBOOLE_1:1; :: thesis: verum