let G be _Graph; :: thesis: for f being VColoring of G holds
( f is proper iff for e, v, w being object st e DJoins 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 DJoins v,w,G holds
f . v <> f . w )

hereby :: thesis: ( ( for e, v, w being object st e DJoins 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 DJoins v,w,G holds
f . v <> f . w
let e, v, w be object ; :: thesis: ( e DJoins v,w,G implies f . v <> f . w )
assume e DJoins v,w,G ; :: thesis: f . v <> f . w
then e Joins v,w,G by GLIB_000:16;
hence f . v <> f . w by A1, Th10; :: thesis: verum

end;

assume A2: for e, v, w being object st e DJoins v,w,G holds
f . v <> f . w ; :: thesis: f is proper

now :: 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 . b₂ <> f . b₃ )
assume e Joins v,w,G ; :: thesis: f . b₂ <> f . b₃

per cases then ( e DJoins v,w,G or e DJoins w,v,G ) by GLIB_000:16;

suppose e DJoins v,w,G ; :: thesis: f . b₂ <> f . b₃

hence f . v <> f . w by A2; :: thesis: verum

end;

suppose e DJoins w,v,G ; :: thesis: f . b₂ <> f . b₃

hence f . v <> f . w by A2; :: thesis: verum

end;

end;

end;

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