let H be Supergraph of G; :: thesis: not H is finite-vcolorable
G is Subgraph of H by GLIB_006:57;
hence not H is finite-vcolorable ; :: thesis: verum