let G be _Graph; :: thesis: ( G is edgeless iff G .vChromaticNum() = 1 )

hereby :: thesis: ( G .vChromaticNum() = 1 implies G is edgeless )

assume A1: G is edgeless ; :: thesis: G .vChromaticNum() = 1
then A2: G .vChromaticNum() c= 1 by Th57;
1 c= G .vChromaticNum() by A1, Th59;
hence G .vChromaticNum() = 1 by A2, XBOOLE_0:def 10; :: thesis: verum

end;

assume A3: G .vChromaticNum() = 1 ; :: thesis: G is edgeless
then G is loopless ;
then G is 1 -vcolorable by A3, Th54;
hence G is edgeless ; :: thesis: verum