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