theorem :: GLIB_000:38

for G being _Graph
for X1, X2, Y1, Y2 being set st X1 c= X2 & Y1 c= Y2 holds
G .edgesDBetween (X1,Y1) c= G .edgesDBetween (X2,Y2)