let G be _Graph; :: thesis: ( G is loopless implies G is G .vChromaticNum() -vcolorable )
assume G is loopless ; :: thesis: G is G .vChromaticNum() -vcolorable
then ( G is G .order() -vcolorable & G .order() c= G .order() ) by Th29;
then A1: G .order() in H₁(G) ;

now :: thesis: for a being set st a in H₁(G) holds
a is cardinal number

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

end;

then consider c being Cardinal such that
A3: ( c in H₁(G) & c = G .vChromaticNum() ) by A1, GLIBPRE0:14;
consider c9 being cardinal Subset of (G .order()) such that
A4: ( c = c9 & G is c9 -vcolorable ) by A3;
thus G is G .vChromaticNum() -vcolorable by A3, A4; :: thesis: verum