let c be Cardinal; :: thesis: for G2 being c -ecolorable _Graph
for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is c +` 1 -ecolorable
let G2 be c -ecolorable _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 is c +` 1 -ecolorable
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds G1 is c +` 1 -ecolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: G1 is c +` 1 -ecolorable

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

suppose ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 is c +` 1 -ecolorable

then consider G9 being addVertex of G2,w such that
A1: G1 is addEdge of G9,v,e,w by GLIB_006:125;
thus G1 is c +` 1 -ecolorable by A1, Th106; :: thesis: verum

end;

suppose ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ; :: thesis: G1 is c +` 1 -ecolorable

then consider G9 being addVertex of G2,v such that
A2: G1 is addEdge of G9,v,e,w by GLIB_006:126;
thus G1 is c +` 1 -ecolorable by A2, Th106; :: thesis: verum

end;

suppose ( not ( v in the_Vertices_of G2 & not w in the_Vertices_of G2 & not e in the_Edges_of G2 ) & not ( not v in the_Vertices_of G2 & w in the_Vertices_of G2 & not e in the_Edges_of G2 ) ) ; :: thesis: G1 is c +` 1 -ecolorable

then G1 == G2 by GLIB_006:def 12;
then G1 is c -ecolorable by Th103;
hence G1 is c +` 1 -ecolorable by Th99, CARD_2:94; :: thesis: verum

end;

end;