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