card (G .inDegreeMap()) = G .order() by Th59;
hence G .inDegreeMap() is finite ; :: thesis: verum