let G be simple complete _Graph; :: thesis: for v being Vertex of G holds (v .degree()) +` 1 = G .order()
let v be Vertex of G; :: thesis: (v .degree()) +` 1 = G .order()
v in {v} by TARSKI:def 1;
then not v in (the_Vertices_of G) \ {v} by XBOOLE_0:def 5;
then A1: not v in v .allNeighbors() by Th45;
thus (v .degree()) +` 1 = (v .degree()) +` (card {v}) by CARD_1:30
.= (card (v .allNeighbors())) +` (card {v}) by GLIB_008:5
.= card ((v .allNeighbors()) \/ {v}) by A1, ZFMISC_1:50, CARD_2:35
.= card (((the_Vertices_of G) \ {v}) \/ {v}) by Th45
.= G .order() by ZFMISC_1:116 ; :: thesis: verum