let t be TColoring of G; :: thesis: t is pair
consider f being VColoring of G, g being EColoring of G such that
A1: t = [f,g] by Def9;
thus t is pair by A1; :: thesis: verum