let G be _Graph; :: thesis: for c being Cardinal st G is c -vcolorable holds
G .vChromaticNum() c= c
let c be Cardinal; :: thesis: ( G is c -vcolorable implies G .vChromaticNum() c= c )
assume A1: G is c -vcolorable ; :: thesis: G .vChromaticNum() c= c

per cases ( not G .order() in c or G .order() in c ) ;

suppose not G .order() in c ; :: thesis: G .vChromaticNum() c= c

then c c= G .order() by ORDINAL1:16;
then c in H₁(G) by A1;
hence G .vChromaticNum() c= c by SETFAM_1:3; :: thesis: verum

end;

suppose G .order() in c ; :: thesis: G .vChromaticNum() c= c

then G .vChromaticNum() in c by Th56, ORDINAL1:12;
hence G .vChromaticNum() c= c by ORDINAL1:def 2; :: thesis: verum

end;

end;