let G2 be _Graph; :: thesis: for v, e, w being object
for G1 being addEdge of G2,v,e,w holds G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1
let v, e, w be object ; :: thesis: for G1 being addEdge of G2,v,e,w holds G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1
let G1 be addEdge of G2,v,e,w; :: thesis: G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1
G2 is G2 .eChromaticNum() -ecolorable by Lm14;
hence G1 .eChromaticNum() c= (G2 .eChromaticNum()) +` 1 by Th106, Lm15; :: thesis: verum