let G be _Graph; :: thesis: for t being TColoring of G st t _V is proper & t _E is proper & rng (t _V) misses rng (t _E) holds
t is proper
let t be TColoring of G; :: thesis: ( t _V is proper & t _E is proper & rng (t _V) misses rng (t _E) implies t is proper )
assume A1: ( t _V is proper & t _E is proper & rng (t _V) misses rng (t _E) ) ; :: thesis: t is proper

now :: 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 e Joins v,w,G ; :: thesis: (t _V) . v <> (t _E) . e
then ( e in the_Edges_of G & v in the_Vertices_of G ) by GLIB_000:def 13, GLIB_000:13;
then ( e in dom (t _E) & v in dom (t _V) ) by PARTFUN1:def 2;
then ( (t _E) . e in rng (t _E) & (t _V) . v in rng (t _V) ) by FUNCT_1:3;
hence (t _V) . v <> (t _E) . e by A1, XBOOLE_0:3; :: thesis: verum

end;

hence t is proper by A1, Th146; :: thesis: verum