let G be _Graph; :: thesis: for v being Vertex of G holds
( G .minDegree() c= v .degree() & v .degree() c= G .supDegree() & G .minInDegree() c= v .inDegree() & v .inDegree() c= G .supInDegree() & G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() )
let v be Vertex of G; :: thesis: ( G .minDegree() c= v .degree() & v .degree() c= G .supDegree() & G .minInDegree() c= v .inDegree() & v .inDegree() c= G .supInDegree() & G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() )
v .degree() in { (w .degree()) where w is Vertex of G : verum } ;
hence ( G .minDegree() c= v .degree() & v .degree() c= G .supDegree() ) by ZFMISC_1:74, SETFAM_1:3; :: thesis: ( G .minInDegree() c= v .inDegree() & v .inDegree() c= G .supInDegree() & G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() )
v .inDegree() in { (w .inDegree()) where w is Vertex of G : verum } ;
hence ( G .minInDegree() c= v .inDegree() & v .inDegree() c= G .supInDegree() ) by ZFMISC_1:74, SETFAM_1:3; :: thesis: ( G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() )
v .outDegree() in { (w .outDegree()) where w is Vertex of G : verum } ;
hence ( G .minOutDegree() c= v .outDegree() & v .outDegree() c= G .supOutDegree() ) by ZFMISC_1:74, SETFAM_1:3; :: thesis: verum