let c be Cardinal; :: thesis: for G being _Graph st G .minDegree() = c & G .supDegree() = c holds
G is c -regular
let G be _Graph; :: thesis: ( G .minDegree() = c & G .supDegree() = c implies G is c -regular )
assume A1: ( G .minDegree() = c & G .supDegree() = c ) ; :: thesis: G is c -regular
let v be Vertex of G; :: according to GLIB_016:def 4 :: thesis: v .degree() = c
( G .minDegree() c= v .degree() & v .degree() c= G .supDegree() ) by GLIB_013:35;
hence v .degree() = c by A1, XBOOLE_0:def 10; :: thesis: verum