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