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-tcolorable iff G2 is finite-tcolorable )
let v, e, w be object ; :: thesis: for G1 being addEdge of G2,v,e,w st v <> w holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )
let G1 be addEdge of G2,v,e,w; :: thesis: ( v <> w implies ( G1 is finite-tcolorable iff G2 is finite-tcolorable ) )
assume A1: v <> w ; :: thesis: ( G1 is finite-tcolorable iff G2 is finite-tcolorable )

hereby :: thesis: ( G2 is finite-tcolorable implies G1 is finite-tcolorable )

assume A2: G1 is finite-tcolorable ; :: thesis: G2 is finite-tcolorable
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is finite-tcolorable by A2; :: thesis: verum

end;

assume G2 is finite-tcolorable ; :: thesis: G1 is finite-tcolorable
then consider n being Nat such that
A3: G2 is n -tcolorable ;
G1 is n +` 2 -tcolorable by A1, A3, Th171;
hence G1 is finite-tcolorable ; :: thesis: verum