theorem :: GLIBPRE0:27

for G being _trivial _Graph
for v being Vertex of G holds
( v .inDegree() = G .size() & v .outDegree() = G .size() & v .degree() = (G .size()) +` (G .size()) )