let G1 be _Graph; :: thesis: for c being Cardinal
for G2 being removeParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let c be Cardinal; :: thesis: for G2 being removeParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G2 be removeParallelEdges of G1; :: thesis: ( G1 is c -vcolorable iff G2 is c -vcolorable )
thus ( G1 is c -vcolorable implies G2 is c -vcolorable ) by Th31; :: thesis: ( G2 is c -vcolorable implies G1 is c -vcolorable )
assume G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable
then consider f2 being VColoring of G2 such that
A1: ( f2 is proper & card (rng f2) c= c ) ;
the_Vertices_of G1 = the_Vertices_of G2 by GLIB_000:def 33;
then reconsider f1 = f2 as VColoring of G1 ;

now :: thesis: for v, w being Vertex of G1 st v,w are_adjacent holds
f1 . v <> f1 . w

let v, w be Vertex of G1; :: thesis: ( v,w are_adjacent implies f1 . v <> f1 . w )
reconsider v9 = v, w9 = w as Vertex of G2 by GLIB_000:def 33;
assume v,w are_adjacent ; :: thesis: f1 . v <> f1 . w
then v9,w9 are_adjacent by GLIBPRE1:75;
hence f1 . v <> f1 . w by A1; :: thesis: verum

end;

then f1 is proper ;
hence G1 is c -vcolorable by A1; :: thesis: verum