let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds G1 .eChromaticNum() = G2 .eChromaticNum()
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G1 .eChromaticNum() = G2 .eChromaticNum()
let G2 be reverseEdgeDirections of G1,E; :: thesis: G1 .eChromaticNum() = G2 .eChromaticNum()
A1: G1 is G1 .eChromaticNum() -ecolorable by Lm14;
for c being Cardinal st G2 is c -ecolorable holds
G1 .eChromaticNum() c= c by Th104, Lm15;
hence G1 .eChromaticNum() = G2 .eChromaticNum() by A1, Th122; :: thesis: verum