let G be _Graph; :: thesis: for c being Cardinal st G is c -vcolorable & ( for d being Cardinal st G is d -vcolorable holds
c c= d ) holds
G .vChromaticNum() = c
let c be Cardinal; :: thesis: ( G is c -vcolorable & ( for d being Cardinal st G is d -vcolorable holds
c c= d ) implies G .vChromaticNum() = c )
assume G is c -vcolorable ; :: thesis: ( ex d being Cardinal st
( G is d -vcolorable & not c c= d ) or G .vChromaticNum() = c )
then A1: ( G .vChromaticNum() c= c & G is loopless ) by Th57;
assume A2: for d being Cardinal st G is d -vcolorable holds
c c= d ; :: thesis: G .vChromaticNum() = c
( G is G .order() -vcolorable & G .order() c= G .order() ) by A1, Th29;
then A3: G .order() in H₁(G) ;

now :: thesis: for x being set st x in H₁(G) holds
c c= x

let x be set ; :: thesis: ( x in H₁(G) implies c c= x )
assume x in H₁(G) ; :: thesis: c c= x
then consider d being cardinal Subset of (G .order()) such that
A4: ( x = d & G is d -vcolorable ) ;
thus c c= x by A2, A4; :: thesis: verum

end;

then c c= G .vChromaticNum() by A3, SETFAM_1:5;
hence G .vChromaticNum() = c by A1, XBOOLE_0:def 10; :: thesis: verum