let G2 be _Graph; :: thesis: for v, w being Vertex of G2
for e being object
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper
let v, w be Vertex of G2; :: thesis: for e being object
for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper
let e be object ; :: thesis: for G1 being addEdge of G2,v,e,w
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper
let G1 be addEdge of G2,v,e,w; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2 st f1 = f2 & v,w are_adjacent & f2 is proper holds
f1 is proper
let f2 be VColoring of G2; :: thesis: ( f1 = f2 & v,w are_adjacent & f2 is proper implies f1 is proper )
assume A1: ( f1 = f2 & v,w are_adjacent & f2 is proper ) ; :: thesis: f1 is proper

per cases ( not e in the_Edges_of G2 or e in the_Edges_of G2 ) ;

suppose A2: not e in the_Edges_of G2 ; :: thesis: f1 is proper

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

let e9, v9, w9 be object ; :: thesis: ( e9 Joins v9,w9,G1 implies f1 . b₂ <> f1 . b₃ )
assume A3: e9 Joins v9,w9,G1 ; :: thesis: f1 . b₂ <> f1 . b₃

per cases then ( e9 Joins v9,w9,G2 or not e9 in the_Edges_of G2 ) by GLIB_006:72;

suppose e9 Joins v9,w9,G2 ; :: thesis: f1 . b₂ <> f1 . b₃

hence f1 . v9 <> f1 . w9 by A1, Th10; :: thesis: verum

end;

suppose not e9 in the_Edges_of G2 ; :: thesis: f1 . b₂ <> f1 . b₃

then A4: ( ( v9 = v & w9 = w ) or ( v9 = w & w9 = v ) ) by A2, A3, GLIB_006:107;
consider e1 being object such that
A5: e1 Joins v,w,G2 by A1, CHORD:def 3;
e1 Joins v9,w9,G2 by A4, A5, GLIB_000:14;
hence f1 . v9 <> f1 . w9 by A1, Th10; :: thesis: verum

end;

end;

end;

hence f1 is proper by Th10; :: thesis: verum

end;

suppose e in the_Edges_of G2 ; :: thesis: f1 is proper

then G1 == G2 by GLIB_006:def 11;
hence f1 is proper by A1, Th16; :: thesis: verum

end;

end;