let G1, G2 be _Graph; :: thesis: for c being Cardinal
for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is c -ecolorable iff G2 is c -ecolorable )
let c be Cardinal; :: thesis: for F being PGraphMapping of G1,G2 st F is isomorphism holds
( G1 is c -ecolorable iff G2 is c -ecolorable )
let F be PGraphMapping of G1,G2; :: thesis: ( F is isomorphism implies ( G1 is c -ecolorable iff G2 is c -ecolorable ) )
assume A1: F is isomorphism ; :: thesis: ( G1 is c -ecolorable iff G2 is c -ecolorable )
then reconsider F0 = F as one-to-one PGraphMapping of G1,G2 ;
F0 " is isomorphism by A1, GLIB_010:75;
hence ( G1 is c -ecolorable implies G2 is c -ecolorable ) by Th110; :: thesis: ( G2 is c -ecolorable implies G1 is c -ecolorable )
thus ( G2 is c -ecolorable implies G1 is c -ecolorable ) by A1, Th110; :: thesis: verum