let G be _Graph; :: thesis: for f being VColoring of G holds
( f is proper iff for e, v, w being object st e Joins v,w,G holds
f . v <> f . w )
let f be VColoring of G; :: thesis: ( f is proper iff for e, v, w being object st e Joins v,w,G holds
f . v <> f . w )

hereby :: thesis: ( ( for e, v, w being object st e Joins v,w,G holds
f . v <> f . w ) implies f is proper )

assume A1: f is proper ; :: thesis: for e, v, w being object st e Joins v,w,G holds
f . v <> f . w
let e, v, w be object ; :: thesis: ( e Joins v,w,G implies f . v <> f . w )
assume A2: e Joins v,w,G ; :: thesis: f . v <> f . w
then reconsider v0 = v, w0 = w as Vertex of G by GLIB_000:13;
v0,w0 are_adjacent by A2, CHORD:def 3;
hence f . v <> f . w by A1; :: thesis: verum

end;

assume A3: for e, v, w being object st e Joins v,w,G holds
f . v <> f . w ; :: thesis: f is proper
let v, w be Vertex of G; :: according to GLCOLO00:def 1 :: thesis: ( v,w are_adjacent implies f . v <> f . w )
assume v,w are_adjacent ; :: thesis: f . v <> f . w
then consider e being object such that
A4: e Joins v,w,G by CHORD:def 3;
thus f . v <> f . w by A3, A4; :: thesis: verum