let G be _Graph; :: thesis: for g being EColoring of G holds
( g is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 )
let g be EColoring of G; :: thesis: ( g is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 )

hereby :: thesis: ( ( for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 ) implies g is proper )

assume A1: g is proper ; :: thesis: for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2
let e1, e2, v, w1, w2 be object ; :: thesis: ( e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 implies e1 = e2 )
assume A2: ( e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 ) ; :: thesis: e1 = e2
then reconsider v = v as Vertex of G by GLIB_000:13;
( e1 in v .edgesInOut() & e2 in v .edgesInOut() ) by A2, GLIB_000:62;
hence e1 = e2 by A1, A2, Th85; :: thesis: verum

end;

assume A3: for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & g . e1 = g . e2 holds
e1 = e2 ; :: thesis: g is proper

now :: thesis: for v being Vertex of G
for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2

let v be Vertex of G; :: thesis: for e1, e2 being object st e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 holds
e1 = e2
let e1, e2 be object ; :: thesis: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 implies e1 = e2 )
assume A4: ( e1 in v .edgesInOut() & e2 in v .edgesInOut() & g . e1 = g . e2 ) ; :: thesis: e1 = e2
then consider v1 being Vertex of G such that
A5: e1 Joins v,v1,G by GLIB_000:64;
consider v2 being Vertex of G such that
A6: e2 Joins v,v2,G by A4, GLIB_000:64;
thus e1 = e2 by A3, A4, A5, A6; :: thesis: verum

end;

hence g is proper by Th85; :: thesis: verum