let G be _Graph; :: thesis: G .vChromaticNum() c= G .order()

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

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

then G .vChromaticNum() = 0 ;
hence G .vChromaticNum() c= G .order() by XBOOLE_1:2; :: thesis: verum

end;

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

then ( G is G .order() -vcolorable & G .order() c= G .order() ) by Th29;
then G .order() in H₁(G) ;
hence G .vChromaticNum() c= G .order() by SETFAM_1:3; :: thesis: verum

end;

end;