let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 is Dregular iff G2 is Dregular )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ( G1 is Dregular iff G2 is Dregular ) )
assume A1: F is Disomorphism ; :: thesis: ( G1 is Dregular iff G2 is Dregular )

hereby :: thesis: ( G2 is Dregular implies G1 is Dregular )

assume G1 is Dregular ; :: thesis: G2 is Dregular
then consider c being Cardinal such that
A2: G1 is c -Dregular ;
G2 is c -Dregular by A1, A2, Th51;
hence G2 is Dregular ; :: thesis: verum

end;

assume G2 is Dregular ; :: thesis: G1 is Dregular
then consider c being Cardinal such that
A3: G2 is c -Dregular ;
G1 is c -Dregular by A1, A3, Th51;
hence G1 is Dregular ; :: thesis: verum