let G1 be addEdge of G,v,e,w; :: thesis: G1 is c -vertex

per cases ( ( v is Vertex of G & w is Vertex of G ) or not v is Vertex of G or not w is Vertex of G ) ;

suppose ( v is Vertex of G & w is Vertex of G ) ; :: thesis: G1 is c -vertex

then the_Vertices_of G = the_Vertices_of G1 by GLIB_006:102;
hence G1 is c -vertex by Th18; :: thesis: verum

end;

suppose ( not v is Vertex of G or not w is Vertex of G ) ; :: thesis: G1 is c -vertex

then G1 == G by GLIB_006:def 11;
hence G1 is c -vertex by Th20; :: thesis: verum

end;

end;