let c be Cardinal; :: thesis: for G being _Graph st G .minInDegree() = c & G .minOutDegree() = c & G .supInDegree() = c & G .supOutDegree() = c holds
G is c -Dregular
let G be _Graph; :: thesis: ( G .minInDegree() = c & G .minOutDegree() = c & G .supInDegree() = c & G .supOutDegree() = c implies G is c -Dregular )
assume A1: ( G .minInDegree() = c & G .minOutDegree() = c & G .supInDegree() = c & G .supOutDegree() = c ) ; :: thesis: G is c -Dregular
let v be Vertex of G; :: according to GLIB_016:def 8 :: thesis: ( v .inDegree() = c & v .outDegree() = c )
( G .minInDegree() c= v .inDegree() & v .inDegree() c= G .supInDegree() ) by GLIB_013:35;
hence v .inDegree() = c by A1, XBOOLE_0:def 10; :: thesis: v .outDegree() = c
( G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() ) by GLIB_013:35;
hence v .outDegree() = c by A1, XBOOLE_0:def 10; :: thesis: verum