let G2 be edgeless _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 .eChromaticNum() = 1
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not v in the_Vertices_of G2 implies G1 .eChromaticNum() = 1 )
assume A1: not v in the_Vertices_of G2 ; :: thesis: G1 .eChromaticNum() = 1
set G3 = the reverseEdgeDirections of G1,{e};
not e in the_Edges_of G2 ;
then the reverseEdgeDirections of G1,{e} is addAdjVertex of G2,w,e,v by GLIBPRE1:66;
then the reverseEdgeDirections of G1,{e} .eChromaticNum() = 1 by A1, Th130;
hence G1 .eChromaticNum() = 1 by Th125; :: thesis: verum