let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 holds
( f1 is proper iff f2 is proper )
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E
for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 holds
( f1 is proper iff f2 is proper )
let G2 be reverseEdgeDirections of G1,E; :: thesis: for f1 being VColoring of G1
for f2 being VColoring of G2 st f1 = f2 holds
( f1 is proper iff f2 is proper )
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2 st f1 = f2 holds
( f1 is proper iff f2 is proper )
let f2 be VColoring of G2; :: thesis: ( f1 = f2 implies ( f1 is proper iff f2 is proper ) )
assume A1: f1 = f2 ; :: thesis: ( f1 is proper iff f2 is proper )
hence ( f1 is proper implies f2 is proper ) by Lm1; :: thesis: ( f2 is proper implies f1 is proper )
G1 is reverseEdgeDirections of G2,E by GLIB_007:3;
hence ( f2 is proper implies f1 is proper ) by A1, Lm1; :: thesis: verum