let G2 be _Graph; :: thesis: for c being Cardinal
for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w st v,w are_adjacent holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let c be Cardinal; :: thesis: for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w st v,w are_adjacent holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let v, w be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,w st v,w are_adjacent holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w st v,w are_adjacent holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G1 be addEdge of G2,v,e,w; :: thesis: ( v,w are_adjacent implies ( G1 is c -vcolorable iff G2 is c -vcolorable ) )
assume A1: v,w are_adjacent ; :: thesis: ( G1 is c -vcolorable iff G2 is c -vcolorable )

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

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

end;

assume G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable
then consider f2 being VColoring of G2 such that
A3: ( f2 is proper & card (rng f2) c= c ) ;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_006:102;
then reconsider f1 = f2 as VColoring of G1 ;
f1 is proper by A1, A3, Th20;
hence G1 is c -vcolorable by A3; :: thesis: verum