let G2 be _Graph; :: thesis: for v being Vertex of G2
for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for t1 being TColoring of G1
for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let t1 be TColoring of G1; :: thesis: for t2 being TColoring of G2
for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let t2 be TColoring of G2; :: thesis: for x, y being object st not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper holds
t1 is proper
let x, y be object ; :: thesis: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 & t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) & not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper implies t1 is proper )
assume that
A1: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) and
A2: ( t1 _V = (t2 _V) +* (w .--> x) & t1 _E = (t2 _E) +* (e .--> y) ) and
A3: ( not y in (rng (t2 _V)) \/ (rng (t2 _E)) & x <> y & x <> (t2 _V) . v & t2 is proper ) ; :: thesis: t1 is proper
set G3 = the reverseEdgeDirections of G1,{e};
A4: the reverseEdgeDirections of G1,{e} is addAdjVertex of G2,w,e,v by A1, GLIBPRE1:66;
the_Vertices_of G1 = the_Vertices_of the reverseEdgeDirections of G1,{e} by GLIB_007:4;
then reconsider f3 = t1 _V as VColoring of the reverseEdgeDirections of G1,{e} ;
the_Edges_of G1 = the_Edges_of the reverseEdgeDirections of G1,{e} by GLIB_007:4;
then reconsider g3 = t1 _E as EColoring of the reverseEdgeDirections of G1,{e} ;
reconsider t3 = [f3,g3] as TColoring of the reverseEdgeDirections of G1,{e} ;
t3 is proper by A1, A2, A3, A4, Th158;
hence t1 is proper by Th153; :: thesis: verum