let G be _Graph; :: thesis: for t being TColoring of G holds
( t is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) )
let t be TColoring of G; :: thesis: ( t is proper iff for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) )
thus ( t is proper implies for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) ) by Th10, Th86, Th146; :: thesis: ( ( for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) ) implies t is proper )
assume A1: for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G holds
( (t _V) . v <> (t _V) . w1 & (t _V) . v <> (t _E) . e1 & ( e1 <> e2 implies (t _E) . e1 <> (t _E) . e2 ) ) ; :: thesis: t is proper
for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _V) . w by A1;
then A2: t _V is proper by Th10;
for e1, e2, v, w1, w2 being object st e1 Joins v,w1,G & e2 Joins v,w2,G & (t _E) . e1 = (t _E) . e2 holds
e1 = e2 by A1;
then A3: t _E is proper by Th86;
for e, v, w being object st e Joins v,w,G holds
(t _V) . v <> (t _E) . e by A1;
hence t is proper by A2, A3, Th146; :: thesis: verum