let G2 be edgeless _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 is 2 -vcolorable
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 is 2 -vcolorable
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not w in the_Vertices_of G2 holds
G1 is 2 -vcolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not w in the_Vertices_of G2 implies G1 is 2 -vcolorable )
assume A1: not w in the_Vertices_of G2 ; :: thesis: G1 is 2 -vcolorable
A2: not e in the_Edges_of G2 ;
set x = the object ;
set y = { the object };
set h1 = (the_Vertices_of G2) --> the object ;
set h2 = w .--> { the object };
set f = ((the_Vertices_of G2) --> the object ) +* (w .--> { the object });
dom (((the_Vertices_of G2) --> the object ) +* (w .--> { the object })) = (dom ((the_Vertices_of G2) --> the object )) \/ (dom (w .--> { the object })) by FUNCT_4:def 1
.= (the_Vertices_of G2) \/ (dom {[w,{ the object }]}) by FUNCT_4:82
.= (the_Vertices_of G2) \/ {w} by RELAT_1:9
.= the_Vertices_of G1 by A1, A2, GLIB_006:def 12 ;
then reconsider f = ((the_Vertices_of G2) --> the object ) +* (w .--> { the object }) as VColoring of G1 by RELAT_1:def 18, PARTFUN1:def 2;

now :: thesis: for e9, v9, w9 being object st e9 DJoins v9,w9,G1 holds
f . v9 <> f . w9

let e9, v9, w9 be object ; :: thesis: ( e9 DJoins v9,w9,G1 implies f . v9 <> f . w9 )
assume A3: e9 DJoins v9,w9,G1 ; :: thesis: f . v9 <> f . w9
the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, GLIB_006:def 12
.= {e} ;
then e9 in {e} by A3, GLIB_000:def 14;
then A4: e9 = e by TARSKI:def 1;
e DJoins v,w,G1 by A1, A2, GLIB_006:131;
then A5: ( v = v9 & w = w9 ) by A3, A4, GLIB_000:125;
v <> w by A1;
then ( f . v = ((the_Vertices_of G2) --> the object ) . v & f . w = { the object } ) by FUNCT_4:83, FUNCT_4:113;
then f . v in f . w ;
hence f . v9 <> f . w9 by A5; :: thesis: verum

end;

then A6: f is proper by Th11;
(rng ((the_Vertices_of G2) --> the object )) \/ (rng (w .--> { the object })) = { the object } \/ (rng (w .--> { the object })) by FUNCOP_1:8
.= { the object } \/ (rng {[w,{ the object }]}) by FUNCT_4:82
.= { the object } \/ {{ the object }} by RELAT_1:9
.= { the object ,{ the object }} by ENUMSET1:1 ;
then A7: card (rng f) c= card { the object ,{ the object }} by FUNCT_4:17, CARD_1:11;
the object in { the object } by TARSKI:def 1;
then the object <> { the object } by ORDINAL1:5;
then card (rng f) c= 2 by A7, CARD_2:57;
hence G1 is 2 -vcolorable by A6; :: thesis: verum