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

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

let x be set ; :: thesis: ( x in H₁(G) implies G .order() c= x )
assume x in H₁(G) ; :: thesis: G .order() c= x
then consider c being cardinal Subset of (G .order()) such that
A4: ( x = c & G is c -vcolorable ) ;
consider f being VColoring of G such that
A5: ( f is proper & card (rng f) c= c ) by A4;
thus G .order() c= x :: thesis: verum

proof

assume not G .order() c= x ; :: thesis: contradiction
then c in G .order() by A4, ORDINAL1:16;
then card (rng f) in G .order() by A5, ORDINAL1:12;
then card (rng f) in card (dom f) by PARTFUN1:def 2;
then card (rng f) <> card (dom f) ;
then not f is one-to-one by CARD_1:70;
then consider v, w being object such that
A6: ( v in dom f & w in dom f & f . v = f . w & v <> w ) by FUNCT_1:def 4;
reconsider v = v, w = w as Vertex of G by A6;
v,w are_adjacent by A2, A6, CHORD:def 6;
hence contradiction by A5, A6; :: thesis: verum

end;

end;

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