let G2 be _Graph; :: thesis: for c being Cardinal
for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v is endvertex & G2 is c -tcolorable holds
G1 is c -tcolorable
let c be Cardinal; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v is endvertex & G2 is c -tcolorable holds
G1 is c -tcolorable
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v is endvertex & G2 is c -tcolorable holds
G1 is c -tcolorable
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v is endvertex & G2 is c -tcolorable holds
G1 is c -tcolorable
let G1 be addAdjVertex of G2,v,e,w; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & v is endvertex & G2 is c -tcolorable implies G1 is c -tcolorable )
assume A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) ; :: thesis: ( not v is endvertex or not G2 is c -tcolorable or G1 is c -tcolorable )
assume A2: ( v is endvertex & G2 is c -tcolorable ) ; :: thesis: G1 is c -tcolorable
then consider t2 being TColoring of G2 such that
A3: ( t2 is proper & card ((rng (t2 _V)) \/ (rng (t2 _E))) c= c ) ;
consider e9 being object such that
A4: ( v .edgesInOut() = {e9} & not e9 Joins v,v,G2 ) by A2, GLIB_000:def 51;
e9 in v .edgesInOut() by A4, TARSKI:def 1;
then consider v9 being Vertex of G2 such that
A5: e9 Joins v,v9,G2 by GLIB_000:64;
set f = (t2 _V) +* (w .--> ((t2 _E) . e9));
set g = (t2 _E) +* (e .--> ((t2 _V) . v9));
reconsider t1 = [((t2 _V) +* (w .--> ((t2 _E) . e9))),((t2 _E) +* (e .--> ((t2 _V) . v9)))] as TColoring of G1 by A1, Th144;

now :: thesis: for e1, e2, u, w1, w2 being object st e1 Joins u,w1,G1 & e2 Joins u,w2,G1 holds
( (t1 _V) . u <> (t1 _V) . w1 & (t1 _V) . u <> (t1 _E) . e1 & ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) )

let e1, e2, u, w1, w2 be object ; :: thesis: ( e1 Joins u,w1,G1 & e2 Joins u,w2,G1 implies ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) ) )
A6: e Joins v,w,G1 by A1, GLIB_006:131;
A7: the_Edges_of G1 = (the_Edges_of G2) \/ {e} by A1, GLIB_006:def 12;
assume A8: ( e1 Joins u,w1,G1 & e2 Joins u,w2,G1 ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) )

per cases then ( ( e1 Joins u,w1,G2 & e2 Joins u,w2,G2 ) or ( e1 Joins u,w1,G2 & not e2 in the_Edges_of G2 ) or ( not e1 in the_Edges_of G2 & e2 Joins u,w2,G2 ) or ( not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2 ) ) by GLIB_006:72;

suppose A9: ( e1 Joins u,w1,G2 & e2 Joins u,w2,G2 ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) )

then ( e1 in the_Edges_of G2 & e2 in the_Edges_of G2 ) by GLIB_000:def 13;
then A10: ( (t1 _E) . e1 = (t2 _E) . e1 & (t1 _E) . e2 = (t2 _E) . e2 ) by A1, FUNCT_4:83;
( u in the_Vertices_of G2 & w1 in the_Vertices_of G2 ) by A9, GLIB_000:13;
then ( (t1 _V) . u = (t2 _V) . u & (t1 _V) . w1 = (t2 _V) . w1 ) by A1, FUNCT_4:83;
hence ( (t1 _V) . u <> (t1 _V) . w1 & (t1 _V) . u <> (t1 _E) . e1 ) by A3, A9, A10, Th148; :: thesis: ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 )
thus ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) by A3, A9, A10, Th148; :: thesis: verum

end;

suppose A11: ( e1 Joins u,w1,G2 & not e2 in the_Edges_of G2 ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies not (t1 _E) . b₁ = (t1 _E) . b₂ ) )

e2 in the_Edges_of G1 by A8, GLIB_000:def 13;
then ( e1 in the_Edges_of G2 & e2 in {e} ) by A7, A11, GLIB_000:def 13, XBOOLE_0:def 3;
then A12: ( e1 <> e & e2 = e ) by A1, TARSKI:def 1;
then A13: ( (t1 _E) . e1 = (t2 _E) . e1 & (t1 _E) . e2 = (t2 _V) . v9 ) by FUNCT_4:83, FUNCT_4:113;
( u in the_Vertices_of G2 & w1 in the_Vertices_of G2 ) by A11, GLIB_000:13;
then ( (t1 _V) . u = (t2 _V) . u & (t1 _V) . w1 = (t2 _V) . w1 ) by A1, FUNCT_4:83;
hence ( (t1 _V) . u <> (t1 _V) . w1 & (t1 _V) . u <> (t1 _E) . e1 ) by A3, A11, A13, Th148; :: thesis: ( e1 <> e2 implies not (t1 _E) . e1 = (t1 _E) . e2 )
assume ( e1 <> e2 & (t1 _E) . e1 = (t1 _E) . e2 ) ; :: thesis: contradiction
then A14: ( (t2 _E) . e1 = (t2 _V) . v9 & e9 Joins v9,v,G2 ) by A5, A13, GLIB_000:14;
u in the_Vertices_of G2 by A11, GLIB_000:13;
then ( u = v & w2 = w ) by A1, A6, A8, A12, GLIB_000:15;
then e1 in v .edgesInOut() by A11, GLIB_000:62;
then e1 = e9 by A4, TARSKI:def 1;
hence contradiction by A3, A14, Th148; :: thesis: verum

end;

suppose A15: ( not e1 in the_Edges_of G2 & e2 Joins u,w2,G2 ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies not (t1 _E) . b₁ = (t1 _E) . b₂ ) )

e1 in the_Edges_of G1 by A8, GLIB_000:def 13;
then ( e2 in the_Edges_of G2 & e1 in {e} ) by A7, A15, GLIB_000:def 13, XBOOLE_0:def 3;
then A16: ( e2 <> e & e1 = e ) by A1, TARSKI:def 1;
then A17: ( (t1 _E) . e2 = (t2 _E) . e2 & (t1 _E) . e1 = (t2 _V) . v9 ) by FUNCT_4:83, FUNCT_4:113;
A18: u in the_Vertices_of G2 by A15, GLIB_000:13;
then A19: (t1 _V) . u = (t2 _V) . u by A1, FUNCT_4:83;
A20: ( u = v & w1 = w ) by A1, A6, A8, A16, A18, GLIB_000:15;
then (t1 _V) . w1 = (t2 _E) . e9 by FUNCT_4:113;
hence (t1 _V) . u <> (t1 _V) . w1 by A3, A5, A19, A20, Th148; :: thesis: ( (t1 _V) . u <> (t1 _E) . e1 & ( e1 <> e2 implies not (t1 _E) . e1 = (t1 _E) . e2 ) )
thus (t1 _V) . u <> (t1 _E) . e1 by A3, A5, A17, A19, A20, Th148; :: thesis: ( e1 <> e2 implies not (t1 _E) . e1 = (t1 _E) . e2 )
assume ( e1 <> e2 & (t1 _E) . e1 = (t1 _E) . e2 ) ; :: thesis: contradiction
then A21: ( (t2 _E) . e2 = (t2 _V) . v9 & e9 Joins v9,v,G2 ) by A5, A17, GLIB_000:14;
e2 in v .edgesInOut() by A15, A20, GLIB_000:62;
then e2 = e9 by A4, TARSKI:def 1;
hence contradiction by A3, A21, Th148; :: thesis: verum

end;

suppose A22: ( not e1 in the_Edges_of G2 & not e2 in the_Edges_of G2 ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) )

A23: v <> w by A1;
( e1 in the_Edges_of G1 & e2 in the_Edges_of G1 ) by A8, GLIB_000:def 13;
then ( e1 in {e} & e2 in {e} ) by A7, A22, XBOOLE_0:def 3;
then A24: ( e2 = e & e1 = e ) by TARSKI:def 1;

per cases then ( ( u = v & w1 = w ) or ( u = w & w1 = v ) ) by A6, A8, GLIB_000:15;

suppose ( u = v & w1 = w ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) )

then A25: ( (t1 _V) . u = (t2 _V) . v & (t1 _V) . w1 = (t2 _E) . e9 ) by A23, FUNCT_4:83, FUNCT_4:113;
hence (t1 _V) . u <> (t1 _V) . w1 by A3, A5, Th148; :: thesis: ( (t1 _V) . u <> (t1 _E) . e1 & ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) )
(t1 _E) . e1 = (t2 _V) . v9 by A24, FUNCT_4:113;
hence (t1 _V) . u <> (t1 _E) . e1 by A3, A5, A25, Th148; :: thesis: ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 )
thus ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) by A24; :: thesis: verum

end;

suppose ( u = w & w1 = v ) ; :: thesis: ( (t1 _V) . b₃ <> (t1 _V) . b₄ & (t1 _V) . b₃ <> (t1 _E) . b₁ & ( b₁ <> b₂ implies (t1 _E) . b₁ <> (t1 _E) . b₂ ) )

then A26: ( (t1 _V) . u = (t2 _E) . e9 & (t1 _V) . w1 = (t2 _V) . v ) by A23, FUNCT_4:83, FUNCT_4:113;
hence (t1 _V) . u <> (t1 _V) . w1 by A3, A5, Th148; :: thesis: ( (t1 _V) . u <> (t1 _E) . e1 & ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) )
( (t1 _E) . e1 = (t2 _V) . v9 & e9 Joins v9,v,G2 ) by A5, A24, FUNCT_4:113, GLIB_000:14;
hence (t1 _V) . u <> (t1 _E) . e1 by A3, A26, Th148; :: thesis: ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 )
thus ( e1 <> e2 implies (t1 _E) . e1 <> (t1 _E) . e2 ) by A24; :: thesis: verum

end;

end;

end;

end;

end;

then A27: t1 is proper by Th148;
( e9 in the_Edges_of G2 & v9 in the_Vertices_of G2 ) by A5, GLIB_000:def 13;
then ( e9 in dom (t2 _E) & v9 in dom (t2 _V) ) by PARTFUN1:def 2;
then ( (t2 _E) . e9 in rng (t2 _E) & (t2 _V) . v9 in rng (t2 _V) ) by FUNCT_1:3;
then A28: ( {((t2 _E) . e9)} c= rng (t2 _E) & {((t2 _V) . v9)} c= rng (t2 _V) ) by ZFMISC_1:31;
A29: ((rng (t2 _V)) \/ {((t2 _E) . e9)}) \/ ((rng (t2 _E)) \/ {((t2 _V) . v9)}) = (((rng (t2 _V)) \/ {((t2 _E) . e9)}) \/ (rng (t2 _E))) \/ {((t2 _V) . v9)} by XBOOLE_1:4
.= (({((t2 _E) . e9)} \/ (rng (t2 _E))) \/ (rng (t2 _V))) \/ {((t2 _V) . v9)} by XBOOLE_1:4
.= ((rng (t2 _E)) \/ (rng (t2 _V))) \/ {((t2 _V) . v9)} by A28, XBOOLE_1:12
.= (rng (t2 _E)) \/ ((rng (t2 _V)) \/ {((t2 _V) . v9)}) by XBOOLE_1:4
.= (rng (t2 _V)) \/ (rng (t2 _E)) by A28, XBOOLE_1:12 ;
( rng (t1 _V) c= (rng (t2 _V)) \/ {((t2 _E) . e9)} & rng (t1 _E) c= (rng (t2 _E)) \/ {((t2 _V) . v9)} ) by Lm19;
then (rng (t1 _V)) \/ (rng (t1 _E)) c= (rng (t2 _V)) \/ (rng (t2 _E)) by A29, XBOOLE_1:13;
then card ((rng (t1 _V)) \/ (rng (t1 _E))) c= card ((rng (t2 _V)) \/ (rng (t2 _E))) by CARD_1:11;
hence G1 is c -tcolorable by A3, A27, XBOOLE_1:1; :: thesis: verum