let E be set ; :: thesis: for G1 being _Graph
for G2 being reverseEdgeDirections of G1,E holds G1 .vChromaticNum() = G2 .vChromaticNum()
let G1 be _Graph; :: thesis: for G2 being reverseEdgeDirections of G1,E holds G1 .vChromaticNum() = G2 .vChromaticNum()
let G2 be reverseEdgeDirections of G1,E; :: thesis: G1 .vChromaticNum() = G2 .vChromaticNum()

now :: thesis: for x being object holds
( ( x in H₁(G1) implies x in H₁(G2) ) & ( x in H₁(G2) implies x in H₁(G1) ) )

let x be object ; :: thesis: ( ( x in H₁(G1) implies x in H₁(G2) ) & ( x in H₁(G2) implies x in H₁(G1) ) )

hereby :: thesis: ( x in H₁(G2) implies x in H₁(G1) )

assume x in H₁(G1) ; :: thesis: x in H₁(G2)
then consider c being cardinal Subset of (G1 .order()) such that
A1: ( x = c & G1 is c -vcolorable ) ;
( G1 .order() = G2 .order() & G2 is c -vcolorable ) by A1, Th33, GLIB_007:24;
hence x in H₁(G2) by A1; :: thesis: verum

end;

assume x in H₁(G2) ; :: thesis: x in H₁(G1)
then consider c being cardinal Subset of (G2 .order()) such that
A2: ( x = c & G2 is c -vcolorable ) ;
( G1 .order() = G2 .order() & G1 is c -vcolorable ) by A2, Th33, GLIB_007:24;
hence x in H₁(G1) by A2; :: thesis: verum

end;

hence G1 .vChromaticNum() = G2 .vChromaticNum() by TARSKI:2; :: thesis: verum