let G be _Graph; :: thesis: ( G is edgeless iff G is 1 -vcolorable )

hereby :: thesis: ( G is 1 -vcolorable implies G is edgeless )

set x = the object ;
set f = (the_Vertices_of G) --> the object ;
reconsider f = (the_Vertices_of G) --> the object as VColoring of G ;
assume G is edgeless ; :: thesis: G is 1 -vcolorable
then for e, v, w being object st e Joins v,w,G holds
f . v <> f . w by GLIB_008:50;
then A1: f is proper by Th10;
card (rng f) c= card { the object } by CARD_1:11, FUNCOP_1:13;
then card (rng f) c= 1 by CARD_1:30;
hence G is 1 -vcolorable by A1; :: thesis: verum

end;

assume G is 1 -vcolorable ; :: thesis: G is edgeless
then consider f being VColoring of G such that
A2: ( f is proper & card (rng f) c= 1 ) ;
0 in card (rng f) by ORDINAL1:14;
then 1 c= card (rng f) by ZFMISC_1:31, CARD_1:49;
then card (rng f) = 1 by A2, XBOOLE_0:def 10
.= card { the object } by CARD_1:30 ;
then consider x being object such that
A3: rng f = {x} by CARD_1:29;
A4: f = (dom f) --> x by A3, FUNCOP_1:9;

now :: thesis: not the_Edges_of G <> {}

set e = the Element of the_Edges_of G;
set v = (the_Source_of G) . the Element of the_Edges_of G;
set w = (the_Target_of G) . the Element of the_Edges_of G;
assume the_Edges_of G <> {} ; :: thesis: contradiction
then A5: the Element of the_Edges_of G Joins (the_Source_of G) . the Element of the_Edges_of G,(the_Target_of G) . the Element of the_Edges_of G,G by GLIB_000:def 13;
then ( (the_Source_of G) . the Element of the_Edges_of G in the_Vertices_of G & (the_Target_of G) . the Element of the_Edges_of G in the_Vertices_of G ) by GLIB_000:13;
then ( (the_Source_of G) . the Element of the_Edges_of G in dom f & (the_Target_of G) . the Element of the_Edges_of G in dom f ) by PARTFUN1:def 2;
then ( f . ((the_Source_of G) . the Element of the_Edges_of G) = x & f . ((the_Target_of G) . the Element of the_Edges_of G) = x ) by A4, FUNCOP_1:7;
hence contradiction by A2, A5, Th10; :: thesis: verum

end;

hence G is edgeless ; :: thesis: verum