let G1, G2 be _Graph; :: thesis: ( G1 == G2 implies G1 .vChromaticNum() = G2 .vChromaticNum() )
assume A1: G1 == G2 ; :: 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
A2: ( x = c & G1 is c -vcolorable ) ;
( G1 .order() = G2 .order() & G2 is c -vcolorable ) by A1, A2, Th32, GLIB_000:90;
hence x in H₁(G2) by A2; :: thesis: verum

end;

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

end;

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