let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for t1 being TColoring of G1
for t2 being TColoring of G2 st t1 = t2 & t1 is proper holds
t2 is proper
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E
for t1 being TColoring of G1
for t2 being TColoring of G2 st t1 = t2 & t1 is proper holds
t2 is proper
let G2 be reverseEdgeDirections of G1,E; :: thesis: for t1 being TColoring of G1
for t2 being TColoring of G2 st t1 = t2 & t1 is proper holds
t2 is proper
let t1 be TColoring of G1; :: thesis: for t2 being TColoring of G2 st t1 = t2 & t1 is proper holds
t2 is proper
let t2 be TColoring of G2; :: thesis: ( t1 = t2 & t1 is proper implies t2 is proper )
assume A1: ( t1 = t2 & t1 is proper ) ; :: thesis: t2 is proper
then A2: t2 _V is proper by Th18;
A3: t2 _E is proper by A1, Th91;

now :: thesis: for e, v, w being object st e Joins v,w,G2 holds
(t2 _V) . v <> (t2 _E) . e

let e, v, w be object ; :: thesis: ( e Joins v,w,G2 implies (t2 _V) . v <> (t2 _E) . e )
assume e Joins v,w,G2 ; :: thesis: (t2 _V) . v <> (t2 _E) . e
then e Joins v,w,G1 by GLIB_007:9;
hence (t2 _V) . v <> (t2 _E) . e by A1, Th146; :: thesis: verum

end;

hence t2 is proper by A2, A3, Th146; :: thesis: verum