let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
G1 .eChromaticNum() = G2 .eChromaticNum()
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies G1 .eChromaticNum() = G2 .eChromaticNum() )
assume A1: F is isomorphism ; :: thesis: G1 .eChromaticNum() = G2 .eChromaticNum()
then reconsider F0 = F as one-to-one PGraphMapping of G1,G2 ;
F0 " is isomorphism by A1, GLIB_010:75;
then A2: G2 .eChromaticNum() c= G1 .eChromaticNum() by Th133;
G1 .eChromaticNum() c= G2 .eChromaticNum() by A1, Th133;
hence G1 .eChromaticNum() = G2 .eChromaticNum() by A2, XBOOLE_0:def 10; :: thesis: verum