let G1, G2 be _Graph; :: thesis: for F being PGraphMapping of G1,G2 st F is Disomorphism holds
( G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .minOutDegree() = G2 .minOutDegree() )
let F be PGraphMapping of G1,G2; :: thesis: ( F is Disomorphism implies ( G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .minOutDegree() = G2 .minOutDegree() ) )
assume A1: F is Disomorphism ; :: thesis: ( G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .minOutDegree() = G2 .minOutDegree() )
then A2: ( dom (F _V) = the_Vertices_of G1 & rng (F _V) = the_Vertices_of G2 ) by GLIB_010:def 11, GLIB_010:def 12;
A3: ( G1 .supInDegree() c= G2 .supInDegree() & G1 .supOutDegree() c= G2 .supOutDegree() ) by A1, Th56;
A4: ( G1 .minInDegree() c= G2 .minInDegree() & G1 .minOutDegree() c= G2 .minOutDegree() ) by A1, A2, Th57;
A5: ( G2 .supInDegree() c= G1 .supInDegree() & G2 .supOutDegree() c= G1 .supOutDegree() ) by A1, Th58;
A6: ( G2 .minInDegree() c= G1 .minInDegree() & G2 .minOutDegree() c= G1 .minOutDegree() ) by A1, A2, Th59;
thus ( G1 .supInDegree() = G2 .supInDegree() & G1 .supOutDegree() = G2 .supOutDegree() & G1 .minInDegree() = G2 .minInDegree() & G1 .minOutDegree() = G2 .minOutDegree() ) by A3, A4, A5, A6, XBOOLE_0:def 10; :: thesis: verum