let G be _Graph; :: thesis: for f being VColoring of G st G is edgeless holds
[f,{}] is TColoring of G
let f be VColoring of G; :: thesis: ( G is edgeless implies [f,{}] is TColoring of G )
assume A1: G is edgeless ; :: thesis: [f,{}] is TColoring of G
reconsider g = id (the_Edges_of G) as EColoring of G ;
g = {} by A1;
hence [f,{}] is TColoring of G by Def9; :: thesis: verum