let G2 be Subgraph of G; :: thesis: ( G2 is spanning implies G2 is c -vertex )
assume G2 is spanning ; :: thesis: G2 is c -vertex
then the_Vertices_of G = the_Vertices_of G2 by GLIB_000:def 33;
hence G2 is c -vertex by Th18; :: thesis: verum