let G be loopless _Graph; :: thesis: 1 c= G .vChromaticNum()
assume not 1 c= G .vChromaticNum() ; :: thesis: contradiction
then G .vChromaticNum() in 1 by ORDINAL1:16;
hence contradiction by CARD_1:49, TARSKI:def 1; :: thesis: verum