G .edgesDBetween (X,Y) c= G .edgesBetween (X,Y) by GLIBPRE0:31;
hence G .edgesDBetween (X,Y) is finite ; :: thesis: verum