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 g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let v be Vertex of G2; :: thesis: for e, w being object
for G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let e, w be object ; :: thesis: for G1 being addAdjVertex of G2,v,e,w
for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let G1 be addAdjVertex of G2,v,e,w; :: thesis: for g1 being EColoring of G1
for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let g1 be EColoring of G1; :: thesis: for g2 being EColoring of G2
for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let g2 be EColoring of G2; :: thesis: for x being object st g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let x be object ; :: thesis: ( g1 = g2 +* (e .--> x) & not x in rng g2 & not e in the_Edges_of G2 & not w in the_Vertices_of G2 & g2 is proper implies g1 is proper )
assume that
A1: ( g1 = g2 +* (e .--> x) & not x in rng g2 ) and
A2: ( not e in the_Edges_of G2 & not w in the_Vertices_of G2 ) and
A3: g2 is proper ; :: thesis: g1 is proper
consider G9 being addVertex of G2,w such that
A4: G1 is addEdge of G9,v,e,w by A2, GLIB_006:125;
A5: the_Edges_of G9 = the_Edges_of G2 by GLIB_006:def 10;
then reconsider g9 = g2 as EColoring of G9 ;
g9 is proper by A3, Th92;
hence g1 is proper by A1, A2, A4, A5, Th93; :: thesis: verum