let G be _Graph; :: thesis: ( not G is loopless iff G .vChromaticNum() = 0 )

hereby :: thesis: ( G .vChromaticNum() = 0 implies not G is loopless )

assume A1: not G is loopless ; :: thesis: G .vChromaticNum() = 0

now :: thesis: for x being object holds not x in H₁(G)

given x being object such that A2: x in H₁(G) ; :: thesis: contradiction
consider c being cardinal Subset of (G .order()) such that
A3: ( x = c & G is c -vcolorable ) by A2;
thus contradiction by A1, A3; :: thesis: verum

end;

hence G .vChromaticNum() = 0 by XBOOLE_0:def 1, SETFAM_1:1; :: thesis: verum

end;

assume A4: ( G .vChromaticNum() = 0 & G is loopless ) ; :: thesis: contradiction

per cases ( H₁(G) = {} or H₁(G) <> {} ) ;

suppose A5: H₁(G) = {} ; :: thesis: contradiction

( G is G .order() -vcolorable & G .order() c= G .order() ) by A4, Th29;
then G .order() in H₁(G) ;
hence contradiction by A5; :: thesis: verum

end;

suppose A6: H₁(G) <> {} ; :: thesis: contradiction

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
A7: ( a = c & G is c -vcolorable ) ;
thus a is cardinal number by A7; :: thesis: verum

end;

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

end;

end;