let G be Dsimple vertex-finite _Graph; :: thesis: for v being Vertex of G holds
( v .inDegree() < G .order() & v .outDegree() < G .order() )
let v be Vertex of G; :: thesis: ( v .inDegree() < G .order() & v .outDegree() < G .order() )
A1: (G .order()) - 1 is Nat by CHORD:1;
not v in v .allNeighbors() by GLIB_000:112;
then A2: ( not v in v .inNeighbors() & not v in v .outNeighbors() ) by XBOOLE_0:def 3;
A3: ( v .inNeighbors() c= (the_Vertices_of G) \ {v} & v .outNeighbors() c= (the_Vertices_of G) \ {v} ) by A2, ZFMISC_1:34;
then card (v .inNeighbors()) <= card ((the_Vertices_of G) \ {v}) by NAT_1:43;
then v .inDegree() <= card ((the_Vertices_of G) \ {v}) by GLIB_000:109;
then v .inDegree() <= (G .order()) - (card {v}) by CARD_2:44;
then v .inDegree() <= (G .order()) - 1 by CARD_1:30;
then v .inDegree() < ((G .order()) - 1) + 1 by A1, NAT_1:13;
hence v .inDegree() < G .order() ; :: thesis: v .outDegree() < G .order()
card (v .outNeighbors()) <= card ((the_Vertices_of G) \ {v}) by A3, NAT_1:43;
then v .outDegree() <= card ((the_Vertices_of G) \ {v}) by GLIB_000:110;
then v .outDegree() <= (G .order()) - (card {v}) by CARD_2:44;
then v .outDegree() <= (G .order()) - 1 by CARD_1:30;
then v .outDegree() < ((G .order()) - 1) + 1 by A1, NAT_1:13;
hence v .outDegree() < G .order() ; :: thesis: verum