let c be Cardinal; :: thesis: for G2 being c -ecolorable _Graph
for v, e, w being object
for G1 being addEdge 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 addEdge of G2,v,e,w holds G1 is c +` 1 -ecolorable
let v, e, w be object ; :: thesis: for G1 being addEdge of G2,v,e,w holds G1 is c +` 1 -ecolorable
let G1 be addEdge of G2,v,e,w; :: thesis: G1 is c +` 1 -ecolorable

per cases ( ( 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 or not w in the_Vertices_of G2 or e in the_Edges_of G2 ) ;

suppose A1: ( 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

consider g2 being proper EColoring of G2 such that
A2: card (rng g2) c= c by Def6;
set y = rng g2;
set g1 = g2 +* (e .--> (rng g2));
reconsider g1 = g2 +* (e .--> (rng g2)) as EColoring of G1 by A1, Th79;
A3: rng (e .--> (rng g2)) = rng {[e,(rng g2)]} by FUNCT_4:82
.= {(rng g2)} by RELAT_1:9 ;
not rng g2 in rng g2 ;
then reconsider g1 = g1 as proper EColoring of G1 by A1, Th93;
A4: card (rng g1) c= card ((rng g2) \/ {(rng g2)}) by A3, FUNCT_4:17, CARD_1:11;
not rng g2 in rng g2 ;
then card ((rng g2) \/ {(rng g2)}) = (card (rng g2)) +` (card {(rng g2)}) by CARD_2:35, ZFMISC_1:50
.= (card (rng g2)) +` 1 by CARD_1:30 ;
then card ((rng g2) \/ {(rng g2)}) c= c +` 1 by A2, CARD_2:84;
hence G1 is c +` 1 -ecolorable by A4, XBOOLE_1:1; :: thesis: verum

end;

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

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

end;

end;