let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is finite-tcolorable implies G2 is finite-tcolorable )
assume A1: ( G1 == G2 & G1 is finite-tcolorable ) ; :: thesis: G2 is finite-tcolorable
then consider n being Nat such that
A2: G1 is n -tcolorable ;
G2 is n -tcolorable by A1, A2, Th167;
hence G2 is finite-tcolorable ; :: thesis: verum