let G2 be non edgeless _Graph; :: thesis: for v, e, w being object
for G1 being addAdjVertex of G2,v,e,w holds G1 .vChromaticNum() = G2 .vChromaticNum()
let v, e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w holds G1 .vChromaticNum() = G2 .vChromaticNum()
let G1 be addAdjVertex of G2,v,e,w; :: thesis: G1 .vChromaticNum() = G2 .vChromaticNum()

per cases ( not G2 is loopless or G2 is loopless ) ;

suppose not G2 is loopless ; :: thesis: G1 .vChromaticNum() = G2 .vChromaticNum()

then ( G2 .vChromaticNum() = 0 & G1 .vChromaticNum() = 0 ) ;
hence G1 .vChromaticNum() = G2 .vChromaticNum() ; :: thesis: verum

end;

suppose A1: G2 is loopless ; :: thesis: G1 .vChromaticNum() = G2 .vChromaticNum()

now :: thesis: ( G2 is G1 .vChromaticNum() -vcolorable & ( for c being Cardinal st G2 is c -vcolorable holds
G1 .vChromaticNum() c= c ) )

G1 is G1 .vChromaticNum() -vcolorable by A1, Th54;
hence G2 is G1 .vChromaticNum() -vcolorable by Th37; :: thesis: for c being Cardinal st G2 is c -vcolorable holds
G1 .vChromaticNum() c= c
let c be Cardinal; :: thesis: ( G2 is c -vcolorable implies G1 .vChromaticNum() c= c )
assume G2 is c -vcolorable ; :: thesis: G1 .vChromaticNum() c= c
then G1 is c -vcolorable by Th37;
hence G1 .vChromaticNum() c= c by Th57; :: thesis: verum

end;

hence G1 .vChromaticNum() = G2 .vChromaticNum() by Th58; :: thesis: verum

end;

end;