let n be non zero Nat; :: thesis: for v being Vertex of (canCompleteGraph n) holds
( v .inDegree() = v & v .outDegree() = (n - v) - 1 )
let v be Vertex of (canCompleteGraph n); :: thesis: ( v .inDegree() = v & v .outDegree() = (n - v) - 1 )
thus v .inDegree() = card (v .inNeighbors()) by GLIB_000:109
.= card v by Th1
.= v ; :: thesis: v .outDegree() = (n - v) - 1
thus v .outDegree() = card (v .outNeighbors()) by GLIB_000:110
.= card (n \ (succ v)) by Th1
.= n - (card (succ (Segm v))) by ORDINAL1:21, CARD_2:44
.= n - (card (Segm (v + 1))) by NAT_1:38
.= (n - v) - 1 ; :: thesis: verum