let G be _Graph; :: thesis: for t being TColoring of G holds
( t is proper iff ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) ) )
let t be TColoring of G; :: thesis: ( t is proper iff ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) ) )

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

assume A1: t is proper ; :: thesis: ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) )
hence ( t _V is proper & t _E is proper ) ; :: thesis: for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e
let e, v, w be object ; :: thesis: ( e Joins v,w,G implies (t _V) . v <> (t _E) . e )
assume A2: e Joins v,w,G ; :: thesis: (t _V) . v <> (t _E) . e
then reconsider u = v as Vertex of G by GLIB_000:13;
A3: e in u .edgesInOut() by A2, GLIB_000:62;
then e in the_Edges_of G ;
then e in dom (t _E) by PARTFUN1:def 2;
then (t _E) . e in (t _E) .: (u .edgesInOut()) by A3, FUNCT_1:def 6;
hence (t _V) . v <> (t _E) . e by A1; :: thesis: verum

end;

assume A4: ( t _V is proper & t _E is proper & ( for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e ) ) ; :: thesis: t is proper
hence ( t _V is proper & t _E is proper ) ; :: according to GLCOLO00:def 10 :: thesis: for v being Vertex of G holds not (t _V) . v in (t _E) .: (v .edgesInOut())
let v be Vertex of G; :: thesis: not (t _V) . v in (t _E) .: (v .edgesInOut())
assume (t _V) . v in (t _E) .: (v .edgesInOut()) ; :: thesis: contradiction
then consider e being object such that
A5: ( e in dom (t _E) & e in v .edgesInOut() & (t _V) . v = (t _E) . e ) by FUNCT_1:def 6;
consider w being Vertex of G such that
A6: e Joins v,w,G by A5, GLIB_000:64;
thus contradiction by A4, A5, A6; :: thesis: verum