let c be Cardinal; :: thesis: for G2 being non edgeless _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G2 be non edgeless _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds
( G1 is c -vcolorable iff G2 is c -vcolorable )
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( G1 is c -vcolorable iff G2 is c -vcolorable )

hereby :: thesis: ( G2 is c -vcolorable implies G1 is c -vcolorable )

assume A1: G1 is c -vcolorable ; :: thesis: G2 is c -vcolorable
G2 is Subgraph of G1 by GLIB_006:57;
hence G2 is c -vcolorable by A1, Th31; :: thesis: verum

end;

assume A2: G2 is c -vcolorable ; :: thesis: G1 is c -vcolorable

per cases ( ( not e in the_Edges_of G2 & v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) or ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) or ( not ( not e in the_Edges_of G2 & v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) & not ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ) ) ;

suppose ( not e in the_Edges_of G2 & v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) ; :: thesis: G1 is c -vcolorable

hence G1 is c -vcolorable by A2, Lm4; :: thesis: verum

end;

suppose A3: ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ; :: thesis: G1 is c -vcolorable

set G3 = the reverseEdgeDirections of G1,{e};
the reverseEdgeDirections of G1,{e} is addAdjVertex of G2,w,e,v by A3, GLIBPRE1:66;
then the reverseEdgeDirections of G1,{e} is c -vcolorable by A2, A3, Lm4;
hence G1 is c -vcolorable by Th33; :: thesis: verum

end;

suppose ( not ( not e in the_Edges_of G2 & v in the_Vertices_of G2 & not w in the_Vertices_of G2 ) & not ( not e in the_Edges_of G2 & not v in the_Vertices_of G2 & w in the_Vertices_of G2 ) ) ; :: thesis: G1 is c -vcolorable

then G1 == G2 by GLIB_006:def 12;
hence G1 is c -vcolorable by A2, Th32; :: thesis: verum

end;

end;