let G be _Graph; :: thesis: for t being TColoring of G
for H being Subgraph of G holds [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] is TColoring of H
let t be TColoring of G; :: thesis: for H being Subgraph of G holds [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] is TColoring of H
let H be Subgraph of G; :: thesis: [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] is TColoring of H
A1: (t _V) | (the_Vertices_of H) is VColoring of H by Th3;
(t _E) | (the_Edges_of H) is EColoring of H by Th78;
hence [((t _V) | (the_Vertices_of H)),((t _E) | (the_Edges_of H))] is TColoring of H by A1, Def9; :: thesis: verum