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

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

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

end;

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