let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E
for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 holds
( g1 is proper iff g2 is proper )
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E
for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 holds
( g1 is proper iff g2 is proper )
let G2 be reverseEdgeDirections of G1,E; :: thesis: for g1 being EColoring of G1
for g2 being EColoring of G2 st g1 = g2 holds
( g1 is proper iff g2 is proper )
let g1 be EColoring of G1; :: thesis: for g2 being EColoring of G2 st g1 = g2 holds
( g1 is proper iff g2 is proper )
let g2 be EColoring of G2; :: thesis: ( g1 = g2 implies ( g1 is proper iff g2 is proper ) )
assume A1: g1 = g2 ; :: thesis: ( g1 is proper iff g2 is proper )
hence ( g1 is proper implies g2 is proper ) by Lm7; :: thesis: ( g2 is proper implies g1 is proper )
G1 is reverseEdgeDirections of G2,E by GLIB_007:3;
hence ( g2 is proper implies g1 is proper ) by A1, Lm7; :: thesis: verum