let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let v, e, w be object ; :: thesis: for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-vcolorable iff G2 is finite-vcolorable )
let G1 be addEdge of G2,v,e,w; :: thesis: ( v <> w implies ( G1 is finite-vcolorable iff G2 is finite-vcolorable ) )
assume A1: v <> w ; :: 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
A2: G2 is n -vcolorable ;
G1 is n +` 1 -vcolorable by A1, A2, Th36;
hence G1 is finite-vcolorable ; :: thesis: verum