let G1 be _Graph; :: thesis: for c being Cardinal
for G2 being removeDParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let c be Cardinal; :: thesis: for G2 being removeDParallelEdges of G1 holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G2 be removeDParallelEdges 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 A1: G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable
set G3 = the removeParallelEdges of G2;
( the removeParallelEdges of G2 is c -vcolorable & the removeParallelEdges of G2 is removeParallelEdges of G1 ) by A1, Th31, GLIB_009:95;
hence G1 is c -vcolorable by Th40; :: thesis: verum