let c be Cardinal; :: thesis: for G1, G2 being _Graph
for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is c -Dregular iff G2 is c -Dregular )
let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is c -Dregular iff G2 is c -Dregular )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ( G1 is c -Dregular iff G2 is c -Dregular ) )
assume A1: F is Disomorphism ; :: thesis: ( G1 is c -Dregular iff G2 is c -Dregular )
hence ( G1 is c -Dregular implies G2 is c -Dregular ) by Lm3; :: thesis: ( G2 is c -Dregular implies G1 is c -Dregular )
reconsider F0 = F as one-to-one PGraphMapping of G1,G2 by A1;
( F0 " is semi-Dcontinuous & F0 " is isomorphism ) by A1, GLIB_010:75;
hence ( G2 is c -Dregular implies G1 is c -Dregular ) by Lm3; :: thesis: verum