G is G .size() -edge by GLIB_013:def 4;
then G .degreeMap() = the Vertex of G .--> (2 *` (G .size())) by Th61;
hence G .degreeMap() is trivial ; :: thesis: verum