let V be set ; :: thesis: for G2 being _Graph
for v being object
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G2 be _Graph; :: thesis: for v being object
for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let v be object ; :: thesis: for G1 being addAdjVertexAll of G2,v,V holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G1 be addAdjVertexAll of G2,v,V; :: thesis: ( G1 is finite-vcolorable iff G2 is finite-vcolorable )
thus ( G1 is finite-vcolorable implies G2 is finite-vcolorable ) ; :: thesis: ( G2 is finite-vcolorable implies G1 is finite-vcolorable )
assume G2 is finite-vcolorable ; :: thesis: G1 is finite-vcolorable
then consider n being Nat such that
A1: G2 is n -vcolorable ;
G1 is n +` 1 -vcolorable by A1, Th39;
hence G1 is finite-vcolorable ; :: thesis: verum