let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E holds
( G1 is finite-tcolorable iff G2 is finite-tcolorable )
let G2 be reverseEdgeDirections of G1,E; :: thesis: ( G1 is finite-tcolorable iff G2 is finite-tcolorable )

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

assume G1 is finite-tcolorable ; :: thesis: G2 is finite-tcolorable
then consider n being Nat such that
A1: G1 is n -tcolorable ;
G2 is n -tcolorable by A1, Th168;
hence G2 is finite-tcolorable ; :: thesis: verum

end;

assume G2 is finite-tcolorable ; :: thesis: G1 is finite-tcolorable
then consider n being Nat such that
A2: G2 is n -tcolorable ;
thus G1 is finite-tcolorable by A2, Def12, Th168; :: thesis: verum