let G be Dsimple Dcomplete _Graph; :: thesis: for v being Vertex of G holds
( (v .inDegree()) +` 1 = G .order() & (v .outDegree()) +` 1 = G .order() )
let v be Vertex of G; :: thesis: ( (v .inDegree()) +` 1 = G .order() & (v .outDegree()) +` 1 = G .order() )
v in {v} by TARSKI:def 1;
then A1: not v in (the_Vertices_of G) \ {v} by XBOOLE_0:def 5;
then not v in v .inNeighbors() by Th12;
then A2: v .inNeighbors() misses {v} by ZFMISC_1:50;
thus (v .inDegree()) +` 1 = (v .inDegree()) +` (card {v}) by CARD_1:30
.= (card (v .inNeighbors())) +` (card {v}) by GLIB_000:109
.= card ((v .inNeighbors()) \/ {v}) by A2, CARD_2:35
.= card (((the_Vertices_of G) \ {v}) \/ {v}) by Th12
.= G .order() by ZFMISC_1:116 ; :: thesis: (v .outDegree()) +` 1 = G .order()
not v in v .outNeighbors() by A1, Th12;
then A3: v .outNeighbors() misses {v} by ZFMISC_1:50;
thus (v .outDegree()) +` 1 = (v .outDegree()) +` (card {v}) by CARD_1:30
.= (card (v .outNeighbors())) +` (card {v}) by GLIB_000:110
.= card ((v .outNeighbors()) \/ {v}) by A3, CARD_2:35
.= card (((the_Vertices_of G) \ {v}) \/ {v}) by Th12
.= G .order() by ZFMISC_1:116 ; :: thesis: verum