let G2 be _Graph; :: thesis: for v, e being object
for w being Vertex of G2
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 v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let v, e be object ; :: thesis: for w being Vertex of G2
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 v in the_Vertices_of G2 & g2 is proper holds
g1 is proper
let w be Vertex of G2; :: 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 v 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 v 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 v 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 v 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 v 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 v in the_Vertices_of G2 ) and
A3: g2 is proper ; :: thesis: g1 is proper
consider G9 being addVertex of G2,v such that
A4: G1 is addEdge of G9,v,e,w by A2, GLIB_006:126;
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