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 & f1 is proper holds
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 & f1 is proper holds
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 & f1 is proper holds
f2 is proper
let f1 be VColoring of G1; :: thesis: for f2 being VColoring of G2 st f1 = f2 & f1 is proper holds
f2 is proper
let f2 be VColoring of G2; :: thesis: ( f1 = f2 & f1 is proper implies f2 is proper )
assume ( f1 = f2 & f1 is proper ) ; :: thesis: f2 is proper
then for e, v, w being object st e Joins v,w,G2 holds
f2 . v <> f2 . w by Th10, GLIB_007:9;
hence f2 is proper by Th10; :: thesis: verum