let G be simple vertex-finite _Graph; :: thesis: for v being Vertex of G holds v .degree() < G .order()
let v be Vertex of G; :: thesis: v .degree() < G .order()
A1: (G .order()) - 1 is Nat by CHORD:1;
not v in v .allNeighbors() by GLIB_008:6;
then card (v .allNeighbors()) <= card ((the_Vertices_of G) \ {v}) by NAT_1:43, ZFMISC_1:34;
then v .degree() <= card ((the_Vertices_of G) \ {v}) by GLIB_008:5;
then v .degree() <= (G .order()) - (card {v}) by CARD_2:44;
then v .degree() <= (G .order()) - 1 by CARD_1:30;
then v .degree() < ((G .order()) - 1) + 1 by A1, NAT_1:13;
hence v .degree() < G .order() ; :: thesis: verum