let G2 be edgeless _Graph; :: thesis: for v, e being object
for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 is 1 -ecolorable
let v, e be object ; :: thesis: for w being Vertex of G2
for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 is 1 -ecolorable
let w be Vertex of G2; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not v in the_Vertices_of G2 holds
G1 is 1 -ecolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not v in the_Vertices_of G2 implies G1 is 1 -ecolorable )
assume A1: not v in the_Vertices_of G2 ; :: thesis: G1 is 1 -ecolorable
set x = the object ;
set g = (the_Edges_of G1) --> the object ;
A2: dom ((the_Edges_of G1) --> the object ) = the_Edges_of G1 ;
reconsider g = (the_Edges_of G1) --> the object as EColoring of G1 ;
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, GLIB_006:def 12
.= {e} ;
then g is trivial by A2;
then reconsider g = g as proper EColoring of G1 ;
card (rng g) c= card { the object } by FUNCOP_1:13, CARD_1:11;
then card (rng g) c= 1 by CARD_1:30;
hence G1 is 1 -ecolorable ; :: thesis: verum