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