let c be Cardinal; :: thesis: for G1, G2 being _Graph st G1 == G2 & G1 is c -Dregular holds
G2 is c -Dregular
let G1, G2 be _Graph; :: thesis: ( G1 == G2 & G1 is c -Dregular implies G2 is c -Dregular )
assume G1 == G2 ; :: thesis: ( not G1 is c -Dregular or G2 is c -Dregular )
then consider F being PGraphMapping of G1,G2 such that
A1: ( F = id G1 & F is Disomorphism ) by GLIBPRE0:75;
thus ( not G1 is c -Dregular or G2 is c -Dregular ) by A1, Lm3; :: thesis: verum