let v be Vertex of (canCompleteGraph omega); :: thesis: ( v .inDegree() = v & v .outDegree() = omega )
thus v .inDegree() = card (v .inNeighbors()) by GLIB_000:109
.= card v by Th1
.= v ; :: thesis: v .outDegree() = omega
A1: omega \ (succ v) is infinite by RAMSEY_1:4;
thus v .outDegree() = card (v .outNeighbors()) by GLIB_000:110
.= card (omega \ (succ v)) by Th1
.= omega by A1, RAMSEY_1:2 ; :: thesis: verum