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 holds
( t1 is proper iff 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 holds
( t1 is proper iff 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 holds
( t1 is proper iff t2 is proper )
let t1 be TColoring of G1; :: thesis: for t2 being TColoring of G2 st t1 = t2 holds
( t1 is proper iff t2 is proper )
let t2 be TColoring of G2; :: thesis: ( t1 = t2 implies ( t1 is proper iff t2 is proper ) )
assume A1: t1 = t2 ; :: thesis: ( t1 is proper iff t2 is proper )
hence ( t1 is proper implies t2 is proper ) by Lm16; :: thesis: ( t2 is proper implies t1 is proper )
G1 is reverseEdgeDirections of G2,E by GLIB_007:3;
hence ( t2 is proper implies t1 is proper ) by A1, Lm16; :: thesis: verum