let G2 be edgeless _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not w in the_Vertices_of G2 implies G1 .eChromaticNum() = 1 )
assume A1: not w in the_Vertices_of G2 ; :: thesis: G1 .eChromaticNum() = 1

now :: thesis: for c being Cardinal st G1 is c -ecolorable holds
1 c= c

let c be Cardinal; :: thesis: ( G1 is c -ecolorable implies 1 c= c )
assume A2: G1 is c -ecolorable ; :: thesis: 1 c= c
assume not 1 c= c ; :: thesis: contradiction
then c in {0} by CARD_1:49, ORDINAL1:16;
then A3: c = 0 by TARSKI:def 1;
e in (the_Edges_of G2) \/ {e} by TARSKI:def 1;
then e in the_Edges_of G1 by A1, GLIB_006:def 12;
hence contradiction by A2, A3; :: thesis: verum

end;

hence G1 .eChromaticNum() = 1 by Th122; :: thesis: verum